Context-aware counter abstraction

DOI10.1007/S10703-010-0096-7zbMATH Open1213.68362OpenAlexW2136867104MaRDI QIDQ600978FDOQ600978

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

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.

zbMATH Keywords

symmetry reductionsymbolic model checkingBoolean programs

Mathematics Subject Classification ID

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

Cites Work

• Dynamic partial-order reduction for model checking software
• Verification of Boolean programs with unbounded thread creation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Model Checking Software
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• A symbolic approach to predicate abstraction.
• Heap Decomposition for Concurrent Shape Analysis
• Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
• Symbolic Counter Abstraction for Concurrent Software
• Title not available (Why is that?)
• Title not available (Why is that?)
• Correct Hardware Design and Verification Methods
• Tools and Algorithms for the Construction and Analysis of Systems
• Combining symmetry reduction and under-approximation for symbolic model checking

Cited In (5)

• Symbolic Counter Abstraction for Concurrent Software
• Structural Counter Abstraction
• SAT-Based Model Checking
• Counterexample-guided abstraction refinement for symmetric concurrent programs
• Title not available (Why is that?)

Uses Software

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

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)