8 citations · 26 across the 7 of their papers we have counts for
8 papers
Deciding Serializability in Network Systems
Guy Amir, Mark Barbone, Nicolas Amat +1
We present the SER modeling language for automatically verifying serializability of concurrent programs, i.e., whether every concurrent execution of the program is equivalent to so…
Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan
We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-proce…
On the Complexity of Proving Polyhedral Reductions
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan
We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equival…
SMPT: A Testbed for Reachability Methods in Generalized Petri Nets
Nicolas Amat, Silvano Dal Zilio
SMPT (for Satisfiability Modulo Petri Net) is a model checker for reachability problems in Petri nets. It started as a portfolio of methods to experiment with symbolic model checki…
Leveraging polyhedral reductions for solving Petri net reachability problems
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan
We propose a new method that takes advantage of structural reductions to accelerate the verification of reachability properties on Petri nets. Our approach relies on a state space…
Property Directed Reachability for Generalized Petri Nets
Nicolas Amat, Silvano Dal Zilio, Thomas Hujsa
We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the Property Directed Reachability (PDR) method.…
Accelerating the Computation of Dead and Concurrent Places using Reductions
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan
We propose a new method for accelerating the computation of a concurrency relation, that is all pairs of places in a Petri net that can be marked together. Our approach relies on a…
A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking
Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio
We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some…