Local proofs for global safety properties

DOI10.1007/s10703-008-0063-8zbMath1176.68118OpenAlexW2086460553MaRDI QIDQ1039842

Ariel Cohen, Kedar S. Namjoshi

Publication date: 23 November 2009

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-008-0063-8

zbMATH Keywords

compositionalitymodel checkinglocal proofslocal reasoning

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Local Symmetry and Compositional Verification ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Compositional Reasoning ⋮ Model Checking Concurrent Programs ⋮ Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions ⋮ Analysis of correct synchronization of operating system components ⋮ Compositional reasoning for shared-variable concurrent programs ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays

Uses Software

• CESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modular verification of multithreaded programs
• Counterexample-guided abstraction refinement for symbolic model checking
• Local Proofs for Linear-Time Properties of Concurrent Programs
• Compositional Verification and 3-Valued Abstractions Join Forces
• Precise Thread-Modular Verification
• Verifying properties of parallel programs
• Symmetry and Completeness in the Analysis of Parameterized Systems
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification