An Interpretation of Extensible Objects. - Gérard Boudol; Silvano Dal-Zilio (FCT, 1999)

Spatial Congruence for Ambients Is Decidable. - Silvano Dal-Zilio (ASIAN, 2000)

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

Region Analysis and a pi-Calculus wiht Groups. - Silvano Dal-Zilio; Andrew D. Gordon 001 (MFCS, 2000)

Mobile Processes: A Commented Bibliography. - Silvano Dal-Zilio (MOVEP, 2000)

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

Region analysis and a pi-calculus with groups. - Silvano Dal-Zilio; Andrew D. Gordon 001 (J. Funct. Program., 2002)

On the Dynamics of PB Systems: A Petri Net View. - Silvano Dal-Zilio; Enrico Formenti (Workshop on Membrane Computing, 2003)

XML Schema, Tree Logic and Sheaves Automata. - Silvano Dal-Zilio; Denis Lugiez (RTA, 2003)

Model checking mobile ambients. - Witold Charatonik; Silvano Dal-Zilio; Andrew D. Gordon 001; Supratik Mukhopadhyay; Jean-Marc Talbot (Theor. Comput. Sci., 2003)

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

A logic you can count on. - Silvano Dal-Zilio; Denis Lugiez; Charles Meyssonnier (POPL, 2004)

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

A Typed Calculus for Querying Distributed XML Documents. - Lucia Acciai; Michele Boreale; Silvano Dal-Zilio (TGC, 2006)

Resource control for synchronous cooperative threads. - Roberto M. Amadio; Silvano Dal-Zilio (Theor. Comput. Sci., 2006)

A Concurrent Calculus with Atomic Transactions. - Lucia Acciai; Michele Boreale; Silvano Dal-Zilio (ESOP, 2007)

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

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

An Experiment on Parallel Model Checking of a CTL Fragment. - Rodrigo T. Saad; Silvano Dal-Zilio; Bernard Berthomieu (ATVA, 2012)

Towards timed requirement verification for service choreographies. - Nawal Guermouche; Silvano Dal-Zilio (CollaborateCom, 2012)

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

A Verified Approach for Checking Real-Time Specification Patterns - Nouha Abid; Silvano Dal-Zilio; Didier Le Botlan (CoRR, 2013)

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

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

A formal framework to specify and verify real-time properties on critical systems. - Nouha Abid; Silvano Dal-Zilio; Didier Le Botlan (Int. J. Crit. Comput. Based Syst., 2014)

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

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

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

Real-Time Model Checking Support for AADL. - Bernard Berthomieu; Jean-Paul Bodeveix; Silvano Dal-Zilio; Mamoun Filali; Didier Le Botlan; Guillaume Verdier; François Vernadat 001 (CoRR, 2015)

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

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

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

Symmetry reduction for time Petri net state classes. - Pierre-Alain Bourdil; Bernard Berthomieu; Silvano Dal-Zilio; François Vernadat 001 (Sci. Comput. Program., 2016)

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

Formal verification of user-level real-time property patterns. - Ning Ge 002; Marc Pantel; Silvano Dal-Zilio (TASE, 2017)

Formal verification of complex robotic systems on resource-constrained platforms. - Mohammed Foughali; Bernard Berthomieu; Silvano Dal-Zilio; Pierre-Emmanuel Hladik; Félix Ingrand; Anthony Mallet (FormaliSE@ICSE, 2018)

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

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

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

Presentation of the 9th Edition of the Model Checking Contest. - Elvio Gilberto 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; et al. (TACAS (3), 2019)

MCC: A Tool for Unfolding Colored Petri Nets in PNML Format. - Silvano Dal-Zilio (Petri Nets, 2020)

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

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

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

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

Counting Petri net markings from reduction equations. - Bernard Berthomieu; Didier Le Botlan; Silvano Dal-Zilio (Int. J. Softw. Tools Technol. Transf., 2020)

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

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

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

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

Property Directed Reachability for Generalized Petri Nets. - Nicolas Amat; Silvano Dal-Zilio; Thomas Hujsa (TACAS (1), 2022)

A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking. - Nicolas Amat; Bernard Berthomieu; Silvano Dal-Zilio (Fundam. Informaticae, 2022)

Automated Polyhedral Abstraction Proving. - Nicolas Amat; Silvano Dal-Zilio; Didier Le Botlan (Petri Nets, 2023)

From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Invited Paper). - Sebastian Altmeyer; Étienne André; Silvano Dal-Zilio; Loïc Fejoz; Michael González Harbour; Susanne Graf; J. Javier Gutiérrez; Rafik Henia; Didier Le Botlan; Giuseppe Lipari; Julio L. Medina; Nicolas Navet; et al. (ECRTS, 2023)

SMPT: A Testbed for Reachability Methods in Generalized Petri Nets. - Nicolas Amat; Silvano Dal-Zilio (FM, 2023)

Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023. - Nicolas Amat; Elvio G. Amparore; Bernard Berthomieu; Pierre Bouvier; Silvano Dal-Zilio; Francis Hulin-Hubard; Peter Gjøl Jensen; Loïg Jezequel; Fabrice Kordon; Shuo Li; Emmanuel Paviot-Adet; Laure Petrucci; et al. (TOOLympics@ETAPS, 2023)

From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact). - Sebastian Altmeyer; Étienne André; Silvano Dal-Zilio; Loïc Fejoz; Michael González Harbour; Susanne Graf; J. Javier Gutiérrez; Rafik Henia; Didier Le Botlan; Giuseppe Lipari; Julio L. Medina; Nicolas Navet; et al. (Dagstuhl Artifacts Ser., 2023)

A formal toolchain for offline and run-time verification of robotic systems. - Silvano Dal-Zilio; Pierre-Emmanuel Hladik; Félix Ingrand; Anthony Mallet (Robotics Auton. Syst., 2023)

Leveraging polyhedral reductions for solving Petri net reachability problems. - Nicolas Amat; Silvano Dal-Zilio; Didier Le Botlan (Int. J. Softw. Tools Technol. Transf., 2023)

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability. - Nicolas Amat; Silvano Dal-Zilio; Didier Le Botlan (VMCAI (1), 2024)

On the Complexity of Proving Polyhedral Reductions. - Nicolas Amat; Silvano Dal-Zilio; Didier Le Botlan (Fundam. Informaticae, 2024)