Specification and verification of concurrent programs through refinements

DOI10.1007/S10817-012-9258-1MaRDI QIDQ2351261zbMATH OpenOpenAlexFDO

Authors Sandip Ray, Rob Sumners

Publication date 23 June 2015

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-012-9258-1

zbMATH Keywords

abstractionfairnessreactive systemstheorem provingtrace containment

Mathematics Subject Classification ID

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

• Modular verification for shared-variable concurrent programs
• Refinement for structured concurrent programs
• Automated verification of reactive and concurrent programs by calculation
• Compositional reasoning for shared-variable concurrent programs
• Layered concurrent programs

Cites work

• A mechanically verified incremental garbage collector
• A new solution of Dijkstra's concurrent programming problem
• A symbolic approach to predicate abstraction.
• Algorithms for ordinal arithmetic.
• Computer Aided Verification
• Correct Hardware Design and Verification Methods
• Exact and efficient verification of parameterized cache coherence protocols
• scientific article; zbMATH DE number 1639446 (Why is no real title available?)
• scientific article; zbMATH DE number 1670793 (Why is no real title available?)
• scientific article; zbMATH DE number 1701752 (Why is no real title available?)
• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 88983 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 1744961 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 2087552 (Why is no real title available?)
• scientific article; zbMATH DE number 2090023 (Why is no real title available?)
• scientific article; zbMATH DE number 2102719 (Why is no real title available?)
• scientific article; zbMATH DE number 3071176 (Why is no real title available?)
• Lazy abstraction
• Liveness-preserving simulation relations
• Mechanizing UNITY in Isabelle
• Modeling in Event B. System and software engineering.
• Proving refinement using transduction
• Scheduling multithreaded computations by work stealing
• Temporal verification of reactive systems: response
• The existence of refinement mappings
• Thread scheduling for multiprogrammed multiprocessors

Cited in

(30)

• A perspective on specifying and verifying concurrent modules
• Verification and refinement with fine-grained action-based concurrent objects
• On the role of automated theorem proving in the compile-time derivation of concurrency
• Automated verification of reactive and concurrent programs by calculation
• Refinement for structured concurrent programs
• Stepwise refinement and concurrency: The finite-state case
• Highly dependable concurrent programming using design for verification
• Specification and verification challenges for sequential object-oriented programs
• Specification of parameterized programs -- persistency revisited
• Verification of fine-grain concurrent programs
• A Coq library for verification of concurrent programs
• Verification of parameterized concurrent programs by modular reasoning about data and control
• CSimpl: a rely-guarantee-based framework for verifying concurrent programs
• scientific article; zbMATH DE number 1231598 (Why is no real title available?)
• scientific article; zbMATH DE number 1487742 (Why is no real title available?)
• scientific article; zbMATH DE number 1497787 (Why is no real title available?)
• Refinement-Based Verification of Communicating Unstructured Code
• scientific article; zbMATH DE number 1390334 (Why is no real title available?)
• Formalization of automated trading systems in a concurrent linear framework
• Holistic Specifications for Robust Programs
• Formal verification of language-based concurrent noninterference
• Simulation Refinement for Concurrency Verification
• Robin Milner 1934--2010
• Preface
• Distributed Computing
• Layered concurrent programs
• Modular verification for shared-variable concurrent programs
• A formal system for specification analysis of concurrent programs
• Adequate proof principles for invariance and liveness properties of concurrent programs
• Verification of sequential and concurrent programs

Describes a project that uses

Uses Software

• ACL2
• Rodin
• NQTHM
• UNITY
• VIS

This page was built for publication: Specification and verification of concurrent programs through refinements

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