Publications

Nicolas Amat, Silvano Dal Zilio, Thomas Hujsa (2022). Property Directed Reachability for Generalized Petri Nets. In Proc. of TACAS 2022.

PDF Cite Project DOI

Pierre-Emmanuel Hladik, Félix Ingrand, Silvano Dal Zilio, Reyyan Tekin (2021). Hippo: A formal-model execution engine to control and verify critical real-time systems. Journal of Systems and Software.

Cite Project DOI

Nicolas Amat, Silvano Dal Zilio, Bernard Berthomieu (2021). On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets. In Proc. of ICATPN 2021.

PDF Cite Project DOI

Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan (2021). Accelerating the Computation of Dead and Concurrent Places Using Reductions. In Proc. of SPIN 2021.

PDF Cite Project DOI

Ning Ge, Silvano Dal Zilio, Hongyu Liu, Li Zhang, Lianyi Zhang (2021). RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on μ-calculus. Science of Computer Programming.

Cite Project DOI

Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias (2020). A New Product Construction for the Diagnosability of Patterns in Time Petri Net. In Proc. of CDC 2020.

PDF Cite Project DOI

Silvano Dal Zilio (2020). MCC: a Tool for Unfolding Colored Petri Nets in PNML Format. In Proc. of ICATPN 2020.

PDF Cite Project DOI

Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan (2020). Checking marking reachability with the state equation in Petri net subclasses. unpublished.

Cite Project

Éric Lubat, Silvano Dal Zilio (2020). A Short Overview on Diagnosability of Patterns in Timed Petri Net. In Proc. of MOVEP 2020.

PDF Cite Project

Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan (2020). On the Petri Nets with a Single Shared Place and Beyond. unpublished.

Cite Project

Vincent Mussot, Silvano Dal Zilio, Loïc Correnson, Serge Rainjonneau, Yves Bardout, Grégoire Scano (2020). Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites. In Proc. of ERTSS 2020.

PDF Cite Project

Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias (2019). A State Class Construction for Computing the Intersection of Time Petri Nets Languages. In Proc. of FORMATS 2019.

PDF Cite Project DOI

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 (2019). Presentation of the 9th Edition of the Model Checking Contest. In Proc. of TACAS 2019.

PDF Cite Project DOI

Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio (2019). Counting Petri net markings from reduction equations. International Journal on Software Tools for Technology Transfer (STTT).

Cite Project DOI

Mohammed Foughali, Silvano Dal Zilio, Félix Ingrand (2019). On the Semantics of the GenoM3 Framework. Research Report LAAS.

PDF Cite Project

Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio (2018). Petri Net Reductions for Counting Markings. In Proc. of SPIN 2018.

PDF Cite Project DOI

Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet (2018). Formal Verification of Complex Robotic Systems on Resource-Constrained Platforms. In Proc. of FormaliSE.

PDF Cite Project DOI

Rafael Scarduelli, Pierre-Alain Bourdil, Silvano Dal Zilio, Didier Le Botlan (2018). Time-accurate Middleware for the Virtualization of Communication Protocols. Research Report LAAS.

PDF Cite Project

Alexandre Albore, Silvano Dal Zilio, Marie De Roquemaurel, Christel Seguin, Pierre Virelizier (2018). Timed Formal Model and Verification of Satellite FDIR in Early Design Phase. In Proc. of ERTS 2018.

PDF Cite Project

Ning Ge, Marc Pantel, Silvano Dal Zilio (2017). Formal Verification of User-Level Real-Time Property Patterns. In Proc. of TASE 2017.

PDF Cite Project DOI

Alexandre Albore, Silvano Dal Zilio, Guillaume Infantes, Christel Seguin, Pierre Virelizier (2017). A Model-Checking Approach to Analyse Temporal Failure Propagation with AltaRica. In Proc. of IMBSA 2017.

PDF Cite Project DOI

Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, Félix Ingrand, Anthony Mallet (2016). Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots. In Proc. of ICFEM 2016.

PDF Cite Project DOI

Silvano Dal Zilio, Florent Avellaneda, Jean-Baptiste Raclet (2016). Solving Language Equations Using Flanked Automata. In Proc. of ATVA 2016.

PDF Cite Project DOI

Silvano Dal Zilio, Pierre-Alain Bourdil, Éric Jenn (2016). Building Confidence on Formal Verification Models. In Proc. of SAFECOMP 2016.

PDF Cite Project

Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat (2016). Symmetry reduction for time Petri net state classes. Science of Computer Programming.

PDF Cite Project DOI

Silvano Dal Zilio, Pierre-Alain Bourdil, Éric Jenn (2016). Integrating Model Checking in an Industrial Verification Process: a Structuring Approach. Research Report LAAS.

PDF Cite Project

Pierre-Emmanuel Hladik, Silvano Dal Zilio, Olivier Pasquier, Sébastien Pillement, Bernard Berthomieu (2016). Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées. In Proc. of AFADL 2016.

PDF Cite Project

Silvano Dal Zilio, Jean-Baptiste Raclet, Florent Avellaneda (2015). On the Complexity of Flanked Finite State Automata. Research Report LAAS.

PDF Cite Project

Silvano Dal Zilio, Bernard Berthomieu (2015). Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus. In Proc. of TTCS 2015.

PDF Cite Project DOI

Silvano Dal Zilio, Bernard Berthomieu, Didier Le Botlan (2015). Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina. In Proc. of WATERS 2015.

PDF Cite Project

Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat (2015). Symmetry reduced state classes for time petri nets. In Proc. of SAC 2015.

PDF Cite Project DOI

Silvano Dal Zilio, Bernard Berthomieu, François Vernadat, Mamoun Filali, Jean-Paul Bodeveix, Guillaume Verdier (2015). Real-Time Model Checking Support for AADL. Research Report LAAS.

PDF Cite Project

Lukasz Fronc, Silvano Dal Zilio, Bernard Berthomieu, François Vernadat (2014). Time Petri Nets with Dynamic Firing Dates: Semantics and Applications. In Proc. of FORMATS 2014.

PDF Cite Project DOI

Lukasz Fronc, Silvano Dal Zilio, Bernard Berthomieu (2014). Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre. In Proc. of ABZ 2014: The Landing Gear Case Study.

PDF Cite Project

Lukasz Fronc, Silvano Dal Zilio, Bernard Berthomieu, François Vernadat (2014). Time Petri nets with dynamic firing dates: semantics and applications. Research Report LAAS.

PDF Cite Project

Nouha Abid, Silvano Dal Zilio, Didier Le Botlan (2014). A formal framework to specify and verify real-time properties on critical systems. International Journal of Critical Computer-Based Systems (IJCCBS).

Cite Project DOI

Silvano Dal Zilio, Nawal Guermouche (2012). Towards Timed Requirement Verification for Service Choreographies. In Proc. of CollaborateCom 2012.

PDF Cite Project

Rodrigo Tacla Saad, Silvano Dal Zilio, Bernard Berthomieu (2012). An Experiment on Parallel Model Checking of a CTL Fragment. In Proc. of ATVA 2012.

PDF Cite Project

Nouha Abid, Silvano Dal Zilio, Didier Le Botlan (2012). Real-Time Specification Patterns and Tools. In Proc. of FMICS 2012.

PDF Cite Project DOI

Nouha Abid, Silvano Dal Zilio, Didier Le Botlan (2012). A Verified Approach for Checking Real-Time Specification Patterns. In Proc. of VECoS 2012.

PDF Cite Project

Silvano Dal Zilio, Nouha Abid, Bernard Berthomieu (2012). Who Checks the Model-Checkers?. Research Report LAAS.

PDF Cite Project

Silvano Dal Zilio, Nouha Abid (2012). A Timed Graphical Interval Logic. Research Report LAAS.

PDF Cite Project

Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Mamoun Filali, François Vernadat (2011). Vérification formelle de spécifications AADL via FIACRE. unpublished.

PDF Cite Project

Rodrigo Tacla Saad, Silvano Dal Zilio, Bernard Berthomieu (2011). Mixed Shared-Distributed Hash Tables Approaches for Parallel State Space Construction. In Proc. of ISPDC 2011.

PDF Cite Project DOI

Silvano Dal Zilio, Nouha Abid, Didier Le Botlan (2011). Verification of Real-Time Specification Patterns on Time Transitions Systems. Research Report LAAS.

PDF Cite Project

Silvano Dal Zilio, Nouha Abid, Didier Le Botlan, Bernard Berthomieu, François Vernadat, Mamoun Filali, Jean-Paul Bodeveix (2011). Definition of the Fiacre Real-Time Specification Patterns Language. Research Report Quarteft Project deliverable.

PDF Cite Project

Bernard Berthomieu, Silvano Dal Zilio, Rodrigo Tacla Saad (2010). A General Lock-Free Algorithm for Parallel State Space Construction. In Proc. of PDMC 2010.

PDF Cite Project DOI

Nouha Abid, Silvano Dal Zilio (2010). Real-time Extensions for the Fiacre modeling language. unpublished.

PDF Cite Project

Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Pierre Dissaux, Mamoun Filali, Sébastien Heim, Pierre Gaufillet, François Vernadat (2010). Formal Verification of AADL models with Fiacre and Tina. In Proc. of ERTSS 2010.

PDF Cite Project

Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Mamoun Filali, Marc Pantel, François Vernadat (2010). Langage intermédiaire et transformations de modèles pour le développement de systèmes temps-réel: retour d'expérience sur la chaîne de vérification formelle Fiacre. In Proc. of IDM SafeModel 2010.

PDF Cite Project

Rodrigo Tacla Saad, Silvano Dal Zilio, François Vernadat, Bernard Berthomieu (2009). Enumerative Parallel and Distributed State Space Construction. unpublished.

PDF Cite Project

Bernard Berthomieu, Jean-Paul Bodeveix, Christelle Chaudet, Silvano Dal Zilio, Mamoun Filali, François Vernadat (2009). Formal Verification of AADL Specifications in the Topcased Environment. In Proc. of Ada Europe 2009.

PDF Cite Project DOI

Rodrigo Tacla Saad, François Vernadat, Bernard Berthomieu, Silvano Dal Zilio (2009). Observation Graph implementation for TINA toolbox. In Proc. of EWDC 2009.

PDF Cite Project

Lucia Acciai, Michele Boreale, Silvano Dal Zilio (2007). A Concurrent Calculus with Atomic Transactions. In Proc. of ESOP 2007.

PDF Cite Project DOI

Lucia Acciai, Michele Boreale, Silvano Dal Zilio (2007). A Typed Calculus for Querying Distributed XML Documents. In Proc. of TGC 2006.

PDF Cite Project DOI

Silvano Dal Zilio, Denis Lugiez (2006). XML schema, tree logic and sheaves automata. Applicable Algebra in Engineering, Communication and Computing.

Cite Project DOI

Lucia Acciai, Michele Boreale, Silvano Dal Zilio (2006). A Concurrent Calculus with Atomic Transactions. unpublished.

PDF Cite Project

Roberto M. Amadio, Silvano Dal Zilio (2006). Resource Control for Synchronous Cooperative Threads. Theoretical Computer Science.

Cite Project DOI

Silvano Dal Zilio, Régis Gascon (2005). Resource Bound Certification for a Tail-Recursive Virtual Machine. In Proc. of APLAS 2005.

PDF Cite Project DOI

Lucia Acciai, Michele Boreale, Silvano Dal Zilio (2005). A Typed Calculus for Querying Distributed XML Documents. In Proc. of NWPT 2005.

PDF Cite Project

Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal Zilio, Line Jakubiec (2004). A Functional Scenario for Bytecode Verification of Resource Bounds. In Proc. of CSL 2004.

PDF Cite Project DOI

Roberto M. Amadio, Silvano Dal Zilio (2004). Resource Control for Synchronous Cooperative Threads. In Proc. of CONCUR 2004.

PDF Cite Project DOI

Silvano Dal Zilio, Enrico Formenti (2004). On the Dynamics of PB Systems: A Petri Net View. In Proc. of WMC 2003.

PDF Cite Project DOI

Silvano Dal Zilio, Denis Lugiez, Charles Meyssonnier (2004). A Logic you Can Count On. In Proc. of POPL 2004.

PDF Cite Project DOI

Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal Zilio, Line Jakubiec (2004). A Functional Scenario for Bytecode Verification of Resource Bounds. In Proc. of SPACE 2004.

Cite Project

Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot (2003). Model Checking Mobile Ambients. Theoretical Computer Science.

Cite Project DOI

Silvano Dal Zilio, Denis Lugiez (2003). XML Schema, Tree Logic and Sheaves Automata. In Proc. of RTA 2003.

PDF Cite Project DOI

Silvano Dal Zilio, Denis Lugiez (2002). Multitrees Automata, Presburger's Constraints and Tree Logics. Research Report LIF.

PDF Cite Project

Silvano Dal Zilio, Andrew D. Gordon (2002). Region analysis and a pi-calculus with groups. Journal of Functional Programming.

Cite Project DOI

Silvano Dal Zilio (2001). Fixed Points in the Ambient Logic. In Proc. of FICS 2001.

PDF Cite Project

Silvano Dal Zilio (2001). Mobile Processes: a Commented Bibliography. In Proc. of MOVEP'2K.

PDF Cite Project

Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot (2001). The Complexity of Model Checking Mobile Ambients. In Proc. of FoSSaCS 2001.

PDF Cite Project DOI

Silvano Dal Zilio (2000). Spatial Congruence for the Ambients is Decidable. In Proc. of ASIAN'00.

PDF Cite Project DOI

Silvano Dal Zilio, Andrew D. Gordon (2000). Region analysis and a pi-calculus with groups. In Proc. of MFCS 2000.

PDF Cite Project DOI

Silvano Dal Zilio (2000). An Interpretation of Typed Concurrent Objects in the Blue Calculus. In Proc. of IFIP TCS 2000.

PDF Cite Project DOI

Gérard Boudol, Silvano Dal Zilio (1999). An Interpretation of Extensible Objects. In Proc. of FCT'99.

PDF Cite Project DOI

Silvano Dal Zilio (1999). Le calcul bleu: types et objets. PhD.

PDF Cite Project

Silvano Dal Zilio (1999). A Bisimulation for the Blue Calculus. Research Report INRIA.

PDF Cite Project

Silvano Dal Zilio (1999). Concurrent Objects in the Blue Calculus. In Proc. of JFLA'99.

PDF Cite Project

Silvano Dal Zilio (1998). Quiet and Bouncing Objects: Two Migration Abstractions in a Simple Distributed Blue Calculus. In Proc. of SOAP'98.

PDF Cite Project

Silvano Dal Zilio (1997). Implicit Polymorphic Type System for the Blue Calculus. Research Report INRIA.

PDF Cite Project

Silvano Dal Zilio, Thierry M. Bernard (1995). Learning Binary Shapes as Compression and its Cellular Implementation. In Proc. of ACCV'95.

PDF Cite Project