Efficient coverability analysis by proof minimization

DOI10.1007/978-3-642-32940-1_35MaRDI QIDQ2912699zbMATH OpenOpenAlexFDO

Authors Daniel Kroening, Thomas Wahl, Alexander D. Kaiser

Publication date 25 September 2012

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

Full work available at URL https://doi.org/10.1007/978-3-642-32940-1_35

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Unbounded-thread program verification using thread-state equations
• Verification, Model Checking, and Abstract Interpretation
• Proof spaces for unbounded parallelism
• An SMT-based approach to coverability analysis
• Approaching the coverability problem continuously

Cited in

(10)

• Handling infinitely branching well-structured transition systems
• \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms
• Abstraction-based incremental inductive coverability for Petri nets
• Unbounded-thread program verification using thread-state equations
• Solving Coverability Problem for Monotonic Counter Systems by Supercompilation
• Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States
• Long-Run Average Behavior of Vector Addition Systems with States
• Online Enumeration of All Minimal Inductive Validity Cores
• Invariants for one-counter automata with disequality tests
• Lost in abstraction: monotonicity in multi-threaded programs

Describes a project that uses

Uses Software

• Petruchio

This page was built for publication: Efficient coverability analysis by proof minimization

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