Macquarie University, Sydney Macquarie University ResearchOnline

Showing items 1 - 14 of 14.

Add to Quick Collection   All 14 Results

  • First
  • Previous
  • 1
  • Next
  • Last
Sort:
 Add All Items to Quick Collection
Date: 2012
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/190328
Description: We propose a novel domain-theoretic model for nondeterminism, probability and hidden state, with relations on it that compare information flow. One relation is Smyth-like, based on a structural, refin ... More
Reviewed: Reviewed
Date: 2010
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/148088
Description: We give a quantitative sequential model for noninterference security with probability (but not demonic choice), and a novel refinement order that we prove to be the greatest compositional relation con ... More
Reviewed: Reviewed
Date: 2010
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/1228448
Description: We present a constraint-based method for automatically generating quantitative invariants for linear probabilistic programs, and we show how it can be used, in combination with proof-based methods, to ... More
Reviewed: Reviewed
Date: 2009
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/148619
Description: Security and probability are both artefacts that we hope to bring increasingly within the reach of refinement-based Formal Methods; although we have worked on them separately, in the past, the goal ha ... More
Reviewed: Reviewed
Date: 2007
Language: eng
Resource Type: journal article
Identifier: http://hdl.handle.net/1959.14/25042
Description: The μ-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic (universal) and angelic (existential) choice; its quantitative generalization qMμ e ... More
Reviewed: Reviewed
Date: 2006
Language: eng
Resource Type: journal article
Identifier: http://hdl.handle.net/1959.14/9656
Description: The quantitative μ-calculus qMμ extends the applicability of Kozen's standard μ-calculus [D. Kozen, Results on the propositional μ-calculus, Theoretical Computer Science 27 (1983) 333–354] to probabil ... More
Reviewed: Reviewed
Date: 2006
Language: eng
Resource Type: book chapter
Identifier: http://hdl.handle.net/1959.14/10711
Description: As explained in Chapter 1, Dijkstra’s guarded-command language, which we call <i>GCL</i>, was introduced as an intellectual framework for rigorous reasoning about imperative sequential programs; one o ... More
Date: 2005
Language: eng
Resource Type: journal article
Identifier: http://hdl.handle.net/1959.14/1129909
Description: 7 page(s)
Reviewed: Reviewed
Date: 2005
Language: eng
Resource Type: book
Identifier: http://hdl.handle.net/1959.14/6448
Description: The book is a focused survey on probabilistic program semantics, conceived to tell a coherent story with a uniform notation. It is grouped into three themes: Part I is for 'users' of the techniques wh ... More
Date: 2005
Language: eng
Resource Type: journal article
Identifier: http://hdl.handle.net/1959.14/146586
Description: Herman's Ring [Inform. Process. Lett. 35 (1990) 63; http://www.cs.uiowa.edu/ftp/selfstab/H90.ps.gz] is an algorithm for self-stabilization of N identical processors connected uni-directionally in a sy ... More
Reviewed: Reviewed
Date: 2005
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/161030
Description: In earlier work, we introduced probability to the B by providing a probabilistic choice substitution and by extending B’s semantics to incorporate its meaning [8]. This, a first step, allowed probabil ... More
Reviewed: Reviewed
Date: 2005
Language: eng
Resource Type: journal article
Identifier: http://hdl.handle.net/1959.14/1175308
Description: In Formal Methods we use mathematical structures to model real systems we want to build, or to reason about; in this paper we are concerned principally with game-based models. In an earlier work [Morg ... More
Reviewed: Reviewed
Date: 2005
Language: eng
Resource Type: journal article
Identifier: http://hdl.handle.net/1959.14/8384
Description: The probabilistic guarded-command language (pGCL) contains both demonic and probabilistic non-determinism, which makes it suitable for reasoning about distributed random algorithms. Proofs are based o ... More
Reviewed: Reviewed
Date: 2003
Language: eng
Resource Type: conference paper
Identifier: http://hdl.handle.net/1959.14/1156039
Description: 28 page(s)
Reviewed: Reviewed
  • First
  • Previous
  • 1
  • Next
  • Last