Silvano DAL ZILIO
Silvano DAL ZILIO
Home
Publications
Projects
Courses
Posts
Software
Contact
Light
Dark
Automatic
Tools
Property Directed Reachability for Generalized Petri Nets
We propose a semi-decision procedure for checking generalized reachability properties, on generalized Petri nets, that is based on the …
Nicolas Amat
,
Silvano Dal Zilio
,
Thomas Hujsa
PDF
Cite
Project
DOI
Hippo: A formal-model execution engine to control and verify critical real-time systems
The design of embedded real-time systems requires specific toolchains to guarantee time constraints and safe behavior. These tools and …
Pierre-Emmanuel Hladik
,
Félix Ingrand
,
Silvano Dal Zilio
,
Reyyan Tekin
Cite
Project
DOI
Accelerating the Computation of Dead and Concurrent Places Using Reductions
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 …
Nicolas Amat
,
Silvano Dal Zilio
,
Didier Le Botlan
PDF
Cite
Project
DOI
On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets
We define a method for taking advantage of net reductions in combination with a SMT-based model checker. We prove the correctness of …
Nicolas Amat
,
Silvano Dal Zilio
,
Bernard Berthomieu
PDF
Cite
Project
DOI
A New Product Construction for the Diagnosability of Patterns in Time Petri Net
We propose a method to decide the diagnosability of patterns in labeled Time Petri nets (TPN) that gracefully extends a classic …
Éric Lubat
,
Silvano Dal Zilio
,
Didier Le Botlan
,
Yannick Pencolé
,
Audine Subias
PDF
Cite
Project
DOI
A Short Overview on Diagnosability of Patterns in Timed Petri Net
Diagnosability is a basic property of Discrete Event Systems that relates to the observability of concealed events. Basically, it means …
Éric Lubat
,
Silvano Dal Zilio
PDF
Cite
Project
MCC: a Tool for Unfolding Colored Petri Nets in PNML Format
MCC is a tool designed for a very specific task: to transform the models of High-Level Petri nets, given in the PNML syntax, into …
Silvano Dal Zilio
PDF
Cite
Project
DOI
A State Class Construction for Computing the Intersection of Time Petri Nets Languages
We propose a new method for computing the language intersection of two Time Petri nets (TPN); that is the sequence of labels in timed …
Éric Lubat
,
Silvano Dal Zilio
,
Didier Le Botlan
,
Yannick Pencolé
,
Audine Subias
PDF
Cite
Project
DOI
Counting Petri net markings from reduction equations
We propose a method to count the number of reachable markings of a Petri net without having to enumerate these first. The method relies …
Bernard Berthomieu
,
Didier Le Botlan
,
Silvano Dal Zilio
Cite
Project
DOI
Presentation of the 9th Edition of the Model Checking Contest
The Model Checking Contest (MCC) is an annual competition of software tools for model checking. Tools must process an increasing …
Elvio Amparore
,
Bernard Berthomieu
,
Gianfranco Ciardo
,
Silvano Dal Zilio
,
Francesco Gallà
,
Lom Messan Hillah
,
Francis Hulin-Hubard
,
Peter Gjøl Jensen
,
Loïg Jezequel
,
Fabrice Kordon
,
Didier Le Botlan
,
Torsten Liebke
,
Jeroen Meijer
,
Andrew Miner
,
Emmanuel Paviot-Adet
,
Jiří Srba
,
Yann Thierry-Mieg
,
Tom van Dijk
,
Karsten Wolf
PDF
Cite
Project
DOI
»
Cite
×