Local Proofs for Linear-Time Properties of Concurrent Programs

DOI10.1007/978-3-540-70545-1_15MaRDI QIDQ3512490zbMATH OpenOpenAlexFDO

Authors Ariel Cohen, Kedar S. Namjoshi

Publication date 15 July 2008

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70545-1_15

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Local proofs for global safety properties
• Local Proofs for Global Safety Properties
• A partial approach to model checking
• Model checking concurrent programs
• Proving linearizability with temporal logic

Cited in

(7)

• Local linearizability for concurrent container-type data structures
• Local Proofs for Global Safety Properties
• Local proofs for global safety properties
• Programming Languages and Systems
• Local symmetry and compositional verification
• Commutativity for concurrent program termination proofs
• Compositional reasoning

This page was built for publication: Local Proofs for Linear-Time Properties of Concurrent Programs

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