Accéder directement au contenu

Silvano Dal Zilio

68
Documents
Identifiants chercheurs

Présentation

I was born in France in 1971 and obtained my PhD from INRIA and the University of Nice - Sophia Antipolis in 1999. I hold a Master's Degree in computer science from [École Normale Supérieure de Lyon](http://www.ens-lyon.fr/), where I studied parallel programming and architecture. In 1993, I worked for one year on developing vision and learning algorithms for a *smart retina* for the French ministry of defence, then joined [INRIA Sophia Antipolis](http://www.inria.fr/) for a PhD thesis on using mobile process calculi as a programming model. In 1999, I joined the [Programming Principles and Tools Group](http://research.microsoft.com/research/ppt/) at Microsoft Research in Cambridge (UK) for two years. In 2001, I became a [CNRS](http://www.cnrs.fr/) researcher, working at the [Laboratoire d'Informatique Fondamentale](http://www.lif.univ-mrs.fr/) (LIF) in Marseille, and a member of the INRIA project [MIMOSA](http://www-sop.inria.fr/mimosa/). Since July 2007, I am a CNRS researcher at LAAS-CNRS in Toulouse. **Research topics:**verification of concurrent and distributed systems; safety critical embedded systems; [mobile and higher-order process calculi](http://move.to/mobility); global computation ([mobile ambients](http://www.luca.demon.co.uk/Ambit/Ambit.html)); type systems and static analysis; programming languages for semi-structured data.
I was born in France in 1971 and obtained my PhD from INRIA and the University of Nice - Sophia Antipolis in 1999. I hold a Master's Degree in computer science from [École Normale Supérieure de Lyon](http://www.ens-lyon.fr/), where I studied parallel programming and architecture. In 1993, I worked for one year on developing vision and learning algorithms for a *smart retina* for the French ministry of defence, then joined [INRIA Sophia Antipolis](http://www.inria.fr/) for a PhD thesis on using mobile process calculi as a programming model. In 1999, I joined the [Programming Principles and Tools Group](http://research.microsoft.com/research/ppt/) at Microsoft Research in Cambridge (UK) for two years. In 2001, I became a [CNRS](http://www.cnrs.fr/) researcher, working at the [Laboratoire d'Informatique Fondamentale](http://www.lif.univ-mrs.fr/) (LIF) in Marseille, and a member of the INRIA project [MIMOSA](http://www-sop.inria.fr/mimosa/). Since July 2007, I am a CNRS researcher at LAAS-CNRS in Toulouse. **Research topics:**verification of concurrent and distributed systems; safety critical embedded systems; [mobile and higher-order process calculi](http://move.to/mobility); global computation ([mobile ambients](http://www.luca.demon.co.uk/Ambit/Ambit.html)); type systems and static analysis; programming languages for semi-structured data.

Publications

Image document

A formal toolchain for offline and run-time verification of robotic systems

Silvano Dal Zilio , Pierre-Emmanuel Hladik , Félix Ingrand , Anthony Mallet
Robotics and Autonomous Systems, 2023, 159, pp.104301. ⟨10.1016/j.robot.2022.104301⟩
Article dans une revue hal-03683044v2

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
Dagstuhl Artifacts Series, 2023, 9 (1), ⟨10.4230/DARTS.9.1.4⟩
Article dans une revue hal-04254710v1
Image document

Leveraging polyhedral reductions for solving Petri net reachability problems

Nicolas Amat , Silvano Dal Zilio , Didier Le Botlan
International Journal on Software Tools for Technology Transfer, 2023, 25, pp.95-114. ⟨10.1007/s10009-022-00694-8⟩
Article dans une revue hal-03973463v1
Image document

A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking

Nicolas Amat , Bernard Berthomieu , Silvano Dal Zilio
Fundamenta Informaticae, 2022, 187 (2-4), pp.103-138. ⟨10.3233/FI-222134⟩
Article dans une revue hal-03455697v2
Image document

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
Journal of Systems and Software, 2021, 181, pp.111033. ⟨10.1016/j.jss.2021.111033⟩
Article dans une revue hal-03017661v4

RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on μ-calculus

Ning Ge , Silvano Dal Zilio , Hongyu Liu , Li Zhang , Lianyi Zhang
Science of Computer Programming, 2021, 206, pp.102624. ⟨10.1016/j.scico.2021.102624⟩
Article dans une revue hal-03187896v1
Image document

Counting Petri net markings from reduction equations

Bernard Berthomieu , Didier Le Botlan , Silvano Dal Zilio
International Journal on Software Tools for Technology Transfer, 2020, 22, pp.163-181. ⟨10.1007/s10009-019-00519-1⟩
Article dans une revue hal-02125337v1
Image document

Symmetry reduction for time Petri net state classes

Pierre-Alain Bourdil , Bernard Berthomieu , Silvano Dal Zilio , François Vernadat
Science of Computer Programming, 2016, Science of Computer Programming, 132 (Part 2), pp.209 - 225. ⟨10.1016/j.scico.2016.08.008⟩
Article dans une revue hal-01561994v1
Image document

A Formal Framework to Specify and Verify Real Time Properties on Critical Systems

Didier Le Botlan , Silvano Dal Zilio , Nouha Abid
International Journal of Critical Computer-Based Systems, 2014, 5 (1/2), pp 4-30. ⟨10.1504/IJCCBS.2014.059593⟩
Article dans une revue hal-00941248v1
Image document

XML schema, tree logic and sheaves automata

Silvano Dal Zilio , Denis Lugiez
Applicable Algebra in Engineering, Communication and Computing, 2006, 17, pp.337-377. ⟨10.1007/s00200-006-0016-7⟩
Article dans une revue hal-00109288v1
Image document

Resource Control for Synchronous Cooperative Threads

Roberto M. Amadio , Silvano Dal Zilio
Theoretical Computer Science, 2006, 358, pp.229-254
Article dans une revue hal-00015836v1
Image document

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability

Nicolas Amat , Silvano Dal Zilio , Didier Le Botlan
Verification, Model Checking, and Abstract Interpretation. VMCAI 2024, Jan 2024, London, United Kingdom. pp.101-123, ⟨10.1007/978-3-031-50524-9_5⟩
Communication dans un congrès hal-04375443v1
Image document

Automated Polyhedral Abstraction Proving

Nicolas Amat , Silvano Dal Zilio , Didier Le Botlan
44th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2023), Jun 2023, Lisbon, Portugal. pp.324-345, ⟨10.1007/978-3-031-33620-1_18⟩
Communication dans un congrès hal-04115006v1
Image document

SMPT: A Testbed for Reachability Methods in Generalized Petri Nets

Nicolas Amat , Silvano Dal Zilio
25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.445-453, ⟨10.1007/978-3-031-27481-7_25⟩
Communication dans un congrès hal-04007410v1
Image document

Property Directed Reachability for Generalized Petri Nets

Nicolas Amat , Silvano Dal Zilio , Thomas Hujsa
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022, Apr 2022, Munich, Germany. ⟨10.1007/978-3-030-99524-9_28⟩
Communication dans un congrès hal-03545594v1
Image document

On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets

Nicolas Amat , Bernard Berthomieu , Silvano Dal Zilio
42rd International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2021), Jun 2021, Paris (virtual), France. ⟨10.1007/978-3-030-76983-3_9⟩
Communication dans un congrès hal-03202111v1
Image document

Accelerating the Computation of Dead and Concurrent Places using Reductions

Nicolas Amat , Silvano Dal Zilio , Didier Le Botlan
27th International SPIN Symposium on Model Checking of Software, Jul 2021, Aarhus, Denmark. ⟨10.1007/978-3-030-84629-9_3⟩
Communication dans un congrès hal-03268388v1
Image document

A Short Overview on Diagnosability of Patterns in Timed Petri Net

Éric Lubat , Silvano Dal Zilio
14th Summer School on Modelling and Verification of Parallel Processes (MOVEP 2020), Jun 2020, (on line), France
Communication dans un congrès hal-02899522v1
Image document

Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites

Vincent Mussot , Silvano Dal Zilio , Loic Correnson , Serge Rainjonneau , Yves Bardout
10th European Congress on Embedded Real Time Software and Systems (ERTS 2020), Jan 2020, Toulouse, France
Communication dans un congrès hal-02462058v1
Image document

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
59th Conference on Decision and Control (CDC) 2020, Dec 2020, Jeju Island (virtual conference), South Korea. ⟨10.1109/CDC42340.2020.9303826⟩
Communication dans un congrès hal-02989834v1
Image document

MCC: a Tool for Unfolding Colored Petri Nets in PNML Format

Silvano Dal Zilio
41st International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2020, Paris, France
Communication dans un congrès hal-02511881v1

Presentation of the 9th Edition of the Model Checking Contest

Elvio Amparore , Bernard Berthomieu , Gianfranco Ciardo , Silvano Dal Zilio , Francesco Gallà
Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings, Part III, Apr 2019, Prague, Czech Republic. pp.50-68, ⟨10.1007/978-3-030-17502-3_4⟩
Communication dans un congrès hal-02094047v1
Image document

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
17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Aug 2019, Amsterdam, Netherlands. ⟨10.1007/978-3-030-29662-9_5⟩
Communication dans un congrès hal-02263832v1
Image document

Formal Verification of Complex Robotic Systems on Resource-Constrained Platforms

Mohammed Foughali , Bernard Berthomieu , Silvano Dal Zilio , Pierre-Emmanuel Hladik , Félix Ingrand
FormaliSE: 6th International Conference on Formal Methods in Software Engineering, Jun 2018, Gothenburg, Sweden
Communication dans un congrès hal-01778960v1
Image document

Timed Formal Model and Verification of Satellite FDIR in Early Design Phase

Alexandre Albore , Silvano Dal Zilio , Marie de Roquemaurel , Christel Seguin , Pierre Virelizier
9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Jan 2018, Toulouse, France. 10p
Communication dans un congrès hal-01709008v1
Image document

Petri Net Reductions for Counting Markings

Bernard Berthomieu , Didier Le Botlan , Silvano Dal Zilio
International Symposium on Model Checking Software (SPIN 2018), Jun 2018, Malaga, Spain. ⟨10.1007/978-3-319-94111-0_4⟩
Communication dans un congrès hal-01822078v1
Image document

Formal Verification of User-Level Real-Time Property Patterns

Ning Ge , Marc Pantel , Silvano Dal Zilio
11th International Symposium on Theoretical Aspects of Software Engineering (TASE 2017), Sep 2017, Sophia Antipolis, France. 8p
Communication dans un congrès hal-01589479v1
Image document

A Model-Checking Approach to Analyse Temporal Failure Propagation with AltaRica

Alexandre Albore , Silvano Dal Zilio , Guillaume Infantes , Christel Seguin , Pierre Virelizier
Model-Based Safety and Assessment. IMBSA 2017, Sep 2017, Trento, Italy. 15p., ⟨10.1007/978-3-319-64119-5_10⟩
Communication dans un congrès hal-01693391v2
Image document

Solving Language Equations Using Flanked Automata

Florent Avellaneda , Silvano Dal Zilio , Jean-Baptiste Raclet
ATVA 2016: Automated Technology for Verification and Analysis, Oct 2016, Chiba, Japan. pp.106 - 121, ⟨10.1007/978-3-319-46520-3_7⟩
Communication dans un congrès hal-01202702v2
Image document

Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées

Pierre-Emmanuel Hladik , Silvano Dal Zilio , Olivier Pasquier , Sébastien Pillement , Bernard Berthomieu
15èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Jun 2016, Besançon, France
Communication dans un congrès hal-01331726v1
Image document

Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots

Mohammed Foughali , Bernard Berthomieu , Silvano Dal Zilio , Félix Ingrand , Anthony Mallet
18th International Conference on Formal Engineering Methods (ICFEM 2016), Nov 2016, Tokyo, Japan
Communication dans un congrès hal-01346080v1
Image document

Building Confidence on Formal Verification Models

Pierre-Alain Bourdil , Eric Jenn , Silvano Dal Zilio
Fast Abstracts at International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Sep 2016, Trondheim, Norway
Communication dans un congrès hal-01369144v1
Image document

Simulation of Real-Time Scheduling Algorithms with Cache Effects

Maxime Chéramy , Pierre-Emmanuel Hladik , Anne-Marie Déplanche , Silvano Dal Zilio
6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems, Jul 2015, Lund, Sweden. 6p
Communication dans un congrès hal-01232512v1
Image document

Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus

Silvano Dal Zilio , Bernard Berthomieu
1st International Conference on Theoretical Computer Science (TTCS), Aug 2015, Teheran, Iran. pp.90-104, ⟨10.1007/978-3-319-28678-5_7⟩
Communication dans un congrès hal-01202799v1
Image document

Symmetry reduced state classes for Time Petri nets

Pierre-Alain Bourdil , Bernard Berthomieu , Silvano Dal Zilio , François Vernadat
30th Annual ACM Symposium on Applied Computing, Apr 2015, Salamanca, Spain. pp.1751-1758, ⟨10.1145/2695664.2695803⟩
Communication dans un congrès hal-01275316v1
Image document

Time Petri Nets with Dynamic Firing Dates: Semantics and Applications

Silvano Dal Zilio , Lukasz Fronc , Bernard Berthomieu , François Vernadat
12th International Conference, FORMATS 2014, Sep 2014, Florence, Italy. pp 85-99, ⟨10.1007/978-3-319-10512-3_7⟩
Communication dans un congrès hal-00984354v1
Image document

Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre

Bernard Berthomieu , Silvano Dal Zilio , Lukasz Fronc
4th International ABZ Conference, Jun 2014, France. pp.110-125
Communication dans un congrès hal-00967422v1
Image document

Real-Time Specification Patterns and Tools

Nouha Abid , Silvano Dal Zilio , Didier Le Botlan
17th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2012, Aug 2012, Paris, France. pp. 1-15, ⟨10.1007/978-3-642-32469-7_1⟩
Communication dans un congrès hal-00782649v1
Image document

A Verified Approach to Checking Real-Time Patterns on Fiacre Programs

Nouha Abid , Silvano Dal Zilio
Doctoral Symposium of FM 2012, Aug 2012, Paris, France
Communication dans un congrès hal-01790120v1
Image document

Towards Timed Requirement Verification for Service Choreographies

Nawal Guermouche , Silvano Dal Zilio
8th IEEE International Conference on Collaborative Computing: Networking, Applications and Worksharing, Oct 2012, Pittsburgh, United States. pp.10
Communication dans un congrès hal-00578436v4
Image document

An Experiment on Parallel Model Checking of a CTL Fragment

Rodrigo Tacla Saad , Silvano Dal Zilio , Bernard Berthomieu
10th International Symposium, ATVA 2012, Automated Technology for Verification and Analysis, Oct 2012, Thiruvananthapuram, India. pp.284-299, ⟨10.1007/978-3-642-33386-6_23⟩
Communication dans un congrès hal-00782354v1
Image document

A Verified Approach for Checking Real-Time Specification Patterns

Nouha Abid , Silvano Dal Zilio , Didier Le Botlan
VECoS 2012, 6th International Workshop on Verification and Evaluation of Computer and Communication Systems, Aug 2012, France. pp.11
Communication dans un congrès hal-00782647v2
Image document

Mixed Shared-Distributed Hash Tables Approaches for Parallel State Space Construction

Rodrigo Tacla Saad , Silvano Dal Zilio , Bernard Berthomieu
International Symposium on Parallel and Distributed Computing (ISPDC 2011), Jul 2011, Cluj-Napoca, Romania. 8p
Communication dans un congrès hal-00523188v3
Image document

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

Bernard Berthomieu , Jean-Paul Bodeveix , Silvano Dal Zilio , M Filali , Marc Pantel
IDM 2010 : journées sur l'Ingénierie Dirigée par les Modèles, Mar 2010, Pau, France
Communication dans un congrès hal-00492327v1
Image document

Formal Verification of AADL models with Fiacre and Tina

Bernard Berthomieu , Jean-Paul Bodeveix , Silvano Dal Zilio , Pierre Dissaux , M Filali
ERTSS 2010 - Embedded Real-Time Software and Systems, 3AF Midi-Pyrénées: the French Society of Aeronautic and Aerospace; SEE: the French Society for Electricity, Electronics, and Information & Communication Technologies; SIA: the French Society of Automobive Engineers, May 2010, Toulouse, France. pp.1-9, ⟨10.5281/zenodo.32930⟩
Communication dans un congrès hal-00494348v1
Image document

A General Lock-Free Algorithm for Parallel State Space Construction

Rodrigo Tacla Saad , Silvano Dal Zilio , Bernard Berthomieu
2010 Ninth International Workshop onParallel and Distributed Methods in Verification (PDMC 2010), Second International Workshop on High Performance Computational Systems Biology (HIBI 2010), Sep 2010, Twente, Netherlands. p.8-16, ⟨10.1109/PDMC-HiBi.2010.10⟩
Communication dans un congrès hal-00473072v2

Real-time Extensions for the Fiacre modeling language

Silvano Dal Zilio , Nouha Abid
MoVep 2010, Summer School on Modelling and Verifying Parallel Processes, Jun 2010, Aachen, Germany
Communication dans un congrès hal-00494617v1

Enumerative Parallel and Distributed State Space Construction

Rodrigo Tacla Saad , Bernard Berthomieu , Silvano Dal Zilio , François Vernadat
ETR09 - École d'été Temps Réel, Aug 2009, Paris, France
Communication dans un congrès hal-00494622v1
Image document

Formal Verification of AADL Specifications in the Topcased Environment

Bernard Berthomieu , Jean-Paul Bodeveix , Christelle Chaudet , Silvano Dal Zilio , M Filali
Reliable Software Technologies - Ada Europe 2009, Jun 2009, Brest, France. 15p., ⟨10.1007/978-3-642-01924-1_15⟩
Communication dans un congrès hal-01790208v1
Image document

Observation Graph implementation for TINA toolbox

Rodrigo Tacla Saad , François Vernadat , Bernard Berthomieu , Silvano Dal Zilio
12th European Workshop on Dependable Computing, EWDC 2009, May 2009, Toulouse, France. 4 p
Communication dans un congrès hal-00380671v1
Image document

A Typed Calculus for Querying Distributed XML Documents

Lucia Acciai , Michele Boreale , Silvano Dal Zilio
17th Nordic Workshop on Programming Theory, 2005, Copenhagen, Denmark
Communication dans un congrès hal-00091917v1

A Functional Scenario for Bytecode Verification of Resource Bounds

Roberto Amadio , Solange Coupet-Grimal , Silvano Dal Zilio , Line Jakubiec
Sep 2004, pp.265-279
Communication dans un congrès hal-00146991v1

Resource Control for Synchronous Cooperative Threads

Roberto Amadio , Silvano Dal Zilio
CONCUR Concurrency Theory, Aug 2004, pp.68-82
Communication dans un congrès hal-00146983v1
Image document

Quiet and Bouncing Objects: Two Migration Abstractions in a Simple Distributed Blue Calculus

Silvano Dal Zilio
SOAP'98 -- 1st International Workshop on Semantics of Objects as Processes, 1998, Aalborg, Denmark. pp.7
Communication dans un congrès hal-00091895v1
Image document

Real-time Extensions for the Fiacre modeling language

Nouha Abid , Silvano Dal Zilio
2010, http://automata.rwth-aachen.de/movep2010/index.php?page=about
Autre publication scientifique hal-00593958v1