Abstract
This is a simple framework for expressing linear-time properties. It supports the usual programming constructs (including interleaving parallel composition), equational and inequational reasoning about these, compositional assume/guarantee specifications and refinement, and the mixing of specifications and programs, all shallowly embedded in Isabelle/HOL.
License
Topics
Session ConcurrentHOL
- Strengthen
- HOL_Basis
- Aczel_Sequences
- Lifted_Predicates
- More_Lattices
- Closures
- Galois
- Heyting
- Safety_Logic
- Constructions
- Next_Imp
- Stability
- Refinement
- Programs
- Combinators
- Local_State
- TLS
- ConcurrentHOL
- Atomic
- Exceptions
- Assume_Guarantee
- WickersonDoddsParkinson
- Inhabitation
- FindP
- BFS
- Safety_Closure
- Ix
- Heap
- CImperativeHOL
- TSO
- TSO_Code_Gen
- TSO_litmus
- Floyd_Warshall