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

DOI10.1007/3-540-60043-4_64zbMath1496.68102OpenAlexW1601208182MaRDI QIDQ5096396

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) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

A foundation for modular reasoning about safety and progress properties of state-based concurrent programs ⋮ Modular verification of multithreaded programs

Cites Work

• Unnamed Item
• On using temporal logic for refinement and compositional verification of concurrent systems
• Eliminating the substitution axiom from UNITY logic
• P-A logic - a compositional proof system for distributed programs
• Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
• Derivation of concurrent programs: Two examples
• An axiomatic proof technique for parallel programs
• Composition of assumption-commitment specifications in a UNITY style
• Proofs of Networks of Processes

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