Model checkers based on Petri net coverability have been
used successfully in recent years to verify safety properties of concurrent
shared-memory or asynchronous message-passing software. We revisit a
constraint approach to coverability based on classical Petri net analysis
techniques. We show how to utilize an SMT solver to implement the
constraint approach, and additionally, to generate an inductive invariant from a safety proof. We empirically evaluate our procedure on a
large set of existing Petri net benchmarks. Even though our technique is
incomplete, it can quickly discharge most of the safe instances. Addition-
ally, the inductive invariants computed are usually orders of magnitude
smaller than those produced by existing solvers.
Description
An heuristic to (sometimes) find sufficient invaiants using SMT and search guided by finding solutions for insufficiently strong sets of constraints
AddedBy:raskin
%0 Conference Paper
%1 conf/cav/EsparzaLMMN14
%A Esparza, Javier
%A Ledesma-Garza, Ruslán
%A Majumdar, Rupak
%A Meyer, Philipp J.
%A Niksic, Filip
%B CAV
%D 2014
%E Biere, Armin
%E Bloem, Roderick
%I Springer
%K coverability modelchecking petrinets
%P 603-619
%T An SMT-Based Approach to Coverability Analysis.
%U http://dblp.uni-trier.de/db/conf/cav/cav2014.html#EsparzaLMMN14
%V 8559
%X Model checkers based on Petri net coverability have been
used successfully in recent years to verify safety properties of concurrent
shared-memory or asynchronous message-passing software. We revisit a
constraint approach to coverability based on classical Petri net analysis
techniques. We show how to utilize an SMT solver to implement the
constraint approach, and additionally, to generate an inductive invariant from a safety proof. We empirically evaluate our procedure on a
large set of existing Petri net benchmarks. Even though our technique is
incomplete, it can quickly discharge most of the safe instances. Addition-
ally, the inductive invariants computed are usually orders of magnitude
smaller than those produced by existing solvers.
%@ 978-3-319-08866-2
@inproceedings{conf/cav/EsparzaLMMN14,
abstract = {Model checkers based on Petri net coverability have been
used successfully in recent years to verify safety properties of concurrent
shared-memory or asynchronous message-passing software. We revisit a
constraint approach to coverability based on classical Petri net analysis
techniques. We show how to utilize an SMT solver to implement the
constraint approach, and additionally, to generate an inductive invariant from a safety proof. We empirically evaluate our procedure on a
large set of existing Petri net benchmarks. Even though our technique is
incomplete, it can quickly discharge most of the safe instances. Addition-
ally, the inductive invariants computed are usually orders of magnitude
smaller than those produced by existing solvers.},
added-at = {2018-12-12T15:48:43.000+0100},
author = {Esparza, Javier and Ledesma-Garza, Ruslán and Majumdar, Rupak and Meyer, Philipp J. and Niksic, Filip},
biburl = {https://www.bibsonomy.org/bibtex/24a04e402a6c667122bb1bd993e4b824a/paves_intern},
booktitle = {CAV},
crossref = {conf/cav/2014},
description = {An heuristic to (sometimes) find sufficient invaiants using SMT and search guided by finding solutions for insufficiently strong sets of constraints
AddedBy:raskin},
editor = {Biere, Armin and Bloem, Roderick},
ee = {https://doi.org/10.1007/978-3-319-08867-9_40},
interhash = {68e5bbb2fa4802aa12046879031581e9},
intrahash = {4a04e402a6c667122bb1bd993e4b824a},
isbn = {978-3-319-08866-2},
keywords = {coverability modelchecking petrinets},
pages = {603-619},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
timestamp = {2018-12-12T15:48:43.000+0100},
title = {An SMT-Based Approach to Coverability Analysis.},
url = {http://dblp.uni-trier.de/db/conf/cav/cav2014.html#EsparzaLMMN14},
volume = 8559,
year = 2014
}