An SMT-based approach to coverability analysis

DOI10.1007/978-3-319-08867-9_40MaRDI QIDQ2920990zbMATH OpenOpenAlexFDO

Authors Javier Esparza, Ruslán Ledesma Garza, Philipp J. Meyer, Filip Niksic, Rupak Majumdar

Publication date 29 September 2014

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08867-9_40

Mathematics Subject Classification ID

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

• Approaching the coverability problem continuously
• Abstraction-based incremental inductive coverability for Petri nets
• Efficient implementation of coverability verification on communication-free Petri net

Cited in

(28)

• Commodification of accelerations for the Karp and Miller construction
• Analysis of safeness in a Petri net-based specification of the control part of cyber-physical systems
• Computing parameterized invariants of parameterized Petri nets
• On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
• Abstraction-based incremental inductive coverability for Petri nets
• Directed reachability for infinite-state systems
• Approaching the coverability problem continuously
• Population protocols: beyond runtime analysis
• Unbounded-thread program verification using thread-state equations
• Efficient coverability analysis by proof minimization
• Constraint Solving for Verifying Modal Specifications of Workflow Nets with Data
• Deciding fast termination for probabilistic VASS with nondeterminism
• Applying Step Coverability Trees to Communicating Component-Based Systems
• Solving Coverability Problem for Monotonic Counter Systems by Supercompilation
• Affine extensions of integer vector addition systems with states
• Structural Invariants for the Verification of Systems with Parameterized Architectures
• Computing Parameterized Invariants of Parameterized Petri Nets
• Efficient implementation of coverability verification on communication-free Petri net
• Coverability in 2-VASS with one unary counter is in NP
• Modular rewritable Petri nets: an efficient model for dynamic distributed systems
• Verifying Generalised and Structural Soundness of Workflow Nets via Relaxations
• Property directed reachability for generalized Petri nets
• Abduction of trap invariants in parameterized systems
• Invariants for one-counter automata with disequality tests
• On the length of strongly monotone descending chains over \(\mathbb{N}^d\)
• The complexity of linear temporal verification for continuous counter systems
• Coverability in VASS revisited: improving Rackoff's bounds to obtain conditional optimality
• Monus semantics in vector addition systems with states

Describes a project that uses

Uses Software

• z3

This page was built for publication: An SMT-based approach to coverability analysis

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