Bounded model checking with parametric data structures

DOI10.1016/J.ENTCS.2006.12.019MaRDI QIDQ2864380zbMATH OpenOpenAlexFDO

Authors Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen

Publication date 6 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.12.019

zbMATH Keywords

hybrid automataSATBMCparametric data structures

Mathematics Subject Classification ID

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

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• Bounded parametric model checking for elementary net systems
• Accelerating bounded model checking of safety properties
• Theory and Applications of Models of Computation
• Bounded Model Checking for Parametric Timed Automata

Cites work

• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 1973987 (Why is no real title available?)
• scientific article; zbMATH DE number 2064232 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 1796153 (Why is no real title available?)
• scientific article; zbMATH DE number 1852147 (Why is no real title available?)
• scientific article; zbMATH DE number 2090300 (Why is no real title available?)
• scientific article; zbMATH DE number 2090318 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Accelerating bounded model checking of safety properties
• BerkMin: A fast and robust SAT-solver
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Computer Aided Verification
• Computer Aided Verification
• Efficient distributed SAT and SAT-based distributed bounded model checking
• GRASP: a search algorithm for propositional satisfiability
• The algorithmic analysis of hybrid systems
• Theory and Applications of Satisfiability Testing
• Verification of timed automata via satisfiability checking

Cited in

(8)

• Attacking the Dimensionality Problem of Parameterized Systems via Bounded Reachability Graphs
• Scaling bounded model checking by transforming programs with arrays
• Computer Science Logic
• Lattice-based refinement in bounded model checking
• Efficient loop conditions for bounded model checking hyperproperties
• Communicating Sequential Processes. The First 25 Years
• Verification, Model Checking, and Abstract Interpretation
• Bounded parametric model checking for elementary net systems

Describes a project that uses

Uses Software

• CVC Lite
• BerkMin
• Chaff
• MiniSat

This page was built for publication: Bounded model checking with parametric data structures

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