pGCL

pGCL is both a programming language and a specification language that incorporates both probabilistic and nondeterministic choice, in a unified manner. Program verification is by refinement or annotation (or both), using either Hoare triples, or weakest-precondition entailment, in the style of GCL. This package provides both a shallow embedding of the language primitives, and an annotation and refinement framework. The generated document includes a brief tutorial.


References in zbMATH (referenced in 12 articles )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Hölzl, Johannes: Markov chains and Markov decision processes in Isabelle/HOL (2017)
  2. Hölzl, Johannes: Formalising semantics for expected running time of probabilistic programs (2016)
  3. Lochbihler, Andreas: Probabilistic functions and cryptographic oracles in higher order logic (2016)
  4. Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias: A verified compiler for probability density functions (2015)
  5. Katoen, Joost-Pieter; Gretz, Friedrich; Jansen, Nils; Kaminski, Benjamin Lucien; Olmedo, Federico: Understanding probabilistic programs (2015)
  6. Rand, Robert; Zdancewic, Steve: VPHL: a verified partial-correctness logic for probabilistic programs (2015)
  7. Cock, David: From operational models to information theory; side channels in pGCL with Isabelle (2014)
  8. Klein, Gerwin (ed.); Gamboa, Ruben (ed.): Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings (2014)
  9. Blazy, Sandrine (ed.); Paulin-Mohring, Christine (ed.); Pichardie, David (ed.): Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings (2013)
  10. Cock, David: Practical probability: applying pGCL to lattice scheduling (2013)
  11. Hurd, Joe; McIver, Annabelle; Morgan, Carroll: Probabilistic guarded commands mechanized in HOL (2005)
  12. Hurd, Joe; McIver, Annabelle; Morgan, Carroll: Probabilistic guarded commands mechanized in HOL (2005)