Local Proofs for Linear-Time Properties of Concurrent Programs

DOI10.1007/978-3-540-70545-1_15zbMATH Open1155.68363OpenAlexW1573651116MaRDI QIDQ3512490FDOQ3512490

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

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

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)

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)