Logical foundations for compositional verification and development of concurrent programs in UNITY

DOI10.1007/3-540-60043-4_64MaRDI QIDQ5096396zbMATH OpenOpenAlexFDO

Authors Pierre Collette, Edgar Knapp

Publication date 16 August 2022

Published in Algebraic Methodology and Software Technology (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-60043-4_64

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
• Composition of assumption-commitment specifications in a UNITY style
• On the logic of UNITY
• scientific article; zbMATH DE number 2077135
• scientific article; zbMATH DE number 3956417

Cites work

• An axiomatic proof technique for parallel programs
• 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
• Eliminating the substitution axiom from UNITY logic
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• On using temporal logic for refinement and compositional verification of concurrent systems
• P-A logic - a compositional proof system for distributed programs
• Proofs of Networks of Processes

Cited in

(14)

• The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\)
• Derivation of concurrent programs: Two examples
• Composition of assumption-commitment specifications in a UNITY style
• A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
• UNITY and Büchi automata
• Mechanizing compositional reasoning for concurrent systems: some lessons
• scientific article; zbMATH DE number 176727 (Why is no real title available?)
• Application of the composition principle to unity-like specifications
• Extending the theory of Owicki and Gries with a logic of progress
• Compositionality for tightly coupled systems: a new application of the propositions-as-types interpretation
• Modular verification of multithreaded programs
• Program Development in Computational Logic
• Principles of Distributed Systems
• A modular coding of \textsc{Unity} in \textsc{Coq}

This page was built for publication: Logical foundations for compositional verification and development of concurrent programs in UNITY

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5096396)