Thread-modular abstraction refinement.

DOI10.1007/B11831MaRDI QIDQ5900683zbMATH OpenOpenAlexFDO

Authors Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer

Publication date 20 April 2010

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

Full work available at URL https://doi.org/10.1007/b11831

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1982207
• Symbolic Counter Abstraction for Concurrent Software
• Thread-Modular Verification Is Cartesian Abstract Interpretation
• Modular Safety Checking for Fine-Grained Concurrency
• Counterexample-guided abstraction refinement for symmetric concurrent programs

Cited in

(26)

• Local proofs for global safety properties
• Compositional abstraction refinement for control synthesis
• Compositional reasoning for shared-variable concurrent programs
• Thread-modular analysis of release-acquire concurrency
• Analysis of correct synchronization of operating system components
• Verification of concurrent programs using Petri net unfoldings
• Formalizing and checking thread refinement for data-race-free execution models
• Compositional analysis for verification of parameterized systems
• Verification of SpecC using predicate abstraction
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• Causality-based verification of multi-threaded programs
• Space-reduction strategies for model checking dynamic software
• Model checking concurrent programs
• 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
• Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
• Modular Safety Checking for Fine-Grained Concurrency
• Symbolic Counter Abstraction for Concurrent Software
• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• Thread-modular counterexample-guided abstraction refinement
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
• Lost in abstraction: monotonicity in multi-threaded programs
• CEGAR for compositional analysis of qualitative properties in Markov decision processes
• Automatic analysis of DMA races using model checking and k-induction
• Scaling model checking of dataraces using dynamic information

Describes a project that uses

Uses Software

• BLAST

This page was built for publication: Thread-modular abstraction refinement.

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