Context-aware counter abstraction

DOI10.1007/S10703-010-0096-7MaRDI QIDQ600978zbMATH OpenOpenAlexFDO

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

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

symmetry reductionsymbolic model checkingBoolean programs

Mathematics Subject Classification ID

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

Recommendations

• Symbolic Counter Abstraction for Concurrent Software
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• scientific article; zbMATH DE number 1701765
• Counter abstraction in the CSP/FDR setting
• Model checking: from hardware to software.

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1670768 (Why is no real title available?)
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• scientific article; zbMATH DE number 1487862 (Why is no real title available?)
• scientific article; zbMATH DE number 1903348 (Why is no real title available?)
• A symbolic approach to predicate abstraction.
• Combining symmetry reduction and under-approximation for symbolic model checking
• Correct Hardware Design and Verification Methods
• Dynamic partial-order reduction for model checking software
• Heap Decomposition for Concurrent Shape Analysis
• Model Checking Software
• Symbolic Counter Abstraction for Concurrent Software
• Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification of Boolean programs with unbounded thread creation

Cited in

(7)

• Symbolic Counter Abstraction for Concurrent Software
• Reducing extension edges of concurrent programs for reachability analysis
• Structural Counter Abstraction
• Counter abstraction in the CSP/FDR setting
• SAT-Based Model Checking
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• scientific article; zbMATH DE number 1701765 (Why is no real title available?)

Describes a project that uses

Uses Software

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

This page was built for publication: Context-aware counter abstraction

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