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- (...
প্রধান লেখক: | Hurd, J, McIver, A, Morgan, C |
---|---|
বিন্যাস: | Journal article |
ভাষা: | English |
প্রকাশিত: |
Elsevier
2005
|
বিষয়গুলি: |
অনুরূপ উপাদানগুলি
-
Partial correctness for probabilistic demonic programs
অনুযায়ী: McIver, A, অন্যান্য
প্রকাশিত: (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, অন্যান্য
প্রকাশিত: (2014) -
Precise verification of C programs
অনুযায়ী: Lewis, M
প্রকাশিত: (2014)