Thread-modular model checking

DOI10.1007/3-540-44829-2_14MaRDI QIDQ4426384zbMATH OpenFDO

Authors Cormac Flanagan, Shaz Qadeer

Publication date 16 September 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2648/26480213.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Thread-modular verification for shared-memory programs
• Thread-modular abstraction refinement.
• Precise Thread-Modular Verification
• Model checking of concurrent algorithms: from Java to C
• Thread-Modular Verification Is Cartesian Abstract Interpretation

Cited in

(28)

• Local proofs for global safety properties
• Static analysis of embedded real-time concurrent software with dynamic priorities
• Compositional reasoning for shared-variable concurrent programs
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Thread-modular analysis of release-acquire concurrency
• Analysis of correct synchronization of operating system components
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• Verification of Boolean programs with unbounded thread creation
• Highly dependable concurrent programming using design for verification
• Cloud-based verification of concurrent software
• Model checking with multi-threaded IC3 portfolios
• Causality-based verification of multi-threaded programs
• Space-reduction strategies for model checking dynamic software
• Local symmetry and compositional verification
• Software model checking with explicit scheduler and symbolic threads
• Dataflow analysis for datarace-free programs
• Compositionality Entails Sequentializability
• Compositional reasoning
• LCTD: test-guided proofs for C programs on LLVM
• Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach
• Thread-Modular Verification Is Cartesian Abstract Interpretation
• A model checking-based approach for security policy verification of mobile systems
• Thread-modular verification for shared-memory programs
• Thread modularity at many levels: a pearl in compositional verification
• Model Checking Multithreaded Programs with Asynchronous Atomic Methods
• Thread-modular abstraction refinement.
• Fine-grained complexity of safety verification
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification

This page was built for publication: Thread-modular model checking

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