scientific article; zbMATH DE number 1982207

MaRDI QIDQ4426384zbMATH OpenFDO

Authors Cormac Flanagan, Shaz Qadeer

Publication date 16 September 2003

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

• scientific article; zbMATH DE number 2087551
• 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
• scientific article; zbMATH DE number 2087551 (Why is no real title available?)
• 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:

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