Context-aware counter abstraction

DOI10.1007/s10703-010-0096-7zbMath1213.68362OpenAlexW2136867104MaRDI QIDQ600978

Michele Mazzucchi, Daniel Kroening, Thomas Wahl, Gérard Basler

Publication date: 3 November 2010

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

Full work available at URL: http://hdl.handle.net/20.500.11850/22326

zbMATH Keywords

symbolic model checkingsymmetry reductionBoolean programs

Mathematics Subject Classification ID

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

Related Items

SAT-Based Model Checking, Counterexample-guided abstraction refinement for symmetric concurrent programs

Uses Software

• TopSpin
• SLAM
• SPIN
• CUDD
• SymmSpin
• Bebop
• SatAbs
• DDVerify

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combining symmetry reduction and under-approximation for symbolic model checking
• Verification of Boolean programs with unbounded thread creation
• Heap Decomposition for Concurrent Shape Analysis
• Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
• Symbolic Counter Abstraction for Concurrent Software
• Dynamic partial-order reduction for model checking software
• Model Checking Software
• Correct Hardware Design and Verification Methods
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification