A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
From MaRDI portal
(Redirected from Publication:1391101)
Recommendations
- Logical foundations for compositional verification and development of concurrent programs in UNITY
- scientific article; zbMATH DE number 3956417
- Properties of concurrent programs
- Extending the theory of Owicki and Gries with a logic of progress
- Mechanizing compositional reasoning for concurrent systems: some lessons
Cites work
- A predicate transformer for progress
- Composition of assumption-commitment specifications in a UNITY style
- Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
- Derivation of concurrent programs: Two examples
- DUALITY: A simple formalism for the analysis of UNITY
- Eliminating the substitution axiom from UNITY logic
- scientific article; zbMATH DE number 3926220 (Why is no real title available?)
- scientific article; zbMATH DE number 194539 (Why is no real title available?)
- scientific article; zbMATH DE number 194642 (Why is no real title available?)
- Invariants, composition, and substitution
- Logical foundations for compositional verification and development of concurrent programs in UNITY
- On using temporal logic for refinement and compositional verification of concurrent systems
- P-A logic - a compositional proof system for distributed programs
- Predicate transformers for reasoning about concurrent computation
- Proofs of Networks of Processes
- The existence of refinement mappings
- Unity properties and sequences of states, some observations
Cited in
(10)- UNITY and Büchi automata
- Streamlining progress-based derivations of concurrent programs
- Mechanizing compositional reasoning for concurrent systems: some lessons
- Characterizing progress properties of concurrent objects via contextual refinements
- scientific article; zbMATH DE number 176727 (Why is no real title available?)
- Logical foundations for compositional verification and development of concurrent programs in UNITY
- Extending the theory of Owicki and Gries with a logic of progress
- Modular inference of subprogram contracts for safety checking
- Compositional proofs for concurrent objects
- Towards imperative modules: reasoning about invariants and sharing of mutable state
This page was built for publication: A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1391101)
