Probabilistic guarded commands mechanized in HOL
<p>The probabilistic guarded-command language (<em>pGCL</em>) contains both demonic and probabilistic non-determinism, which makes it suitable for reasoning about distributed random algorithms. Proofs are based on weakest precondition semantics, using an underlying logic of real- (...
Main Authors: | Hurd, J, McIver, A, Morgan, C |
---|---|
格式: | Journal article |
语言: | English |
出版: |
Elsevier
2005
|
主题: |
相似书籍
-
Partial correctness for probabilistic demonic programs
由: McIver, A, et al.
出版: (2001) -
Forward looking logics and automata
由: Ley, C
出版: (2011) -
Automated quantitative software verification
由: Kattenbelt, M
出版: (2010) -
Intersection types and higer-order model checking
由: Ramsay, S, et al.
出版: (2014) -
Precise verification of C programs
由: Lewis, M
出版: (2014)