Skip to Main content

Keywords

BLUE-CALCULUS Abstraction techniques Architecture Description Languages Formal Methods XML SMT solving Model checking Time Petri Nets Real-time requirements Formal methods AADL Model Checking Verification TREE AUTOMATA Formal verification PI-CALCULUS Asynchronous services Parallel State Space Construction Architecture Description Model-checking
› Full list

Co-authors

› Full list

Researcher identifiers

Number of documents

62

Silvano DAL ZILIO

 

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, 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 for a PhD thesis on using mobile process calculi as a programming model.

In 1999, I joined the Programming Principles and Tools Group at Microsoft Research in Cambridge (UK) for two years. In 2001, I became a CNRS researcher, working at the Laboratoire d'Informatique Fondamentale (LIF) in Marseille, and a member of the INRIA project 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; global computation (mobile ambients); type systems and static analysis; programming languages for semi-structured data.

Journal articles7 documents

  • Pierre-Emmanuel Hladik, Félix Ingrand, Silvano Dal Zilio, Reyyan Tekin. Hippo: A Formal-Model Execution Engine to Control and Verify Critical Real-Time Systems. Journal of Systems and Software, Elsevier, 2021, 181, pp.111033. ⟨10.1016/j.jss.2021.111033⟩. ⟨hal-03017661v4⟩
  • Ning Ge, Silvano Dal Zilio, Hongyu Liu, Li Zhang, Lianyi Zhang. RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on μ-calculus. Science of Computer Programming, Elsevier, 2021, 206, pp.102624. ⟨10.1016/j.scico.2021.102624⟩. ⟨hal-03187896⟩
  • Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio. Counting Petri net markings from reduction equations. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2020, 22, pp.163-181. ⟨10.1007/s10009-019-00519-1⟩. ⟨hal-02125337⟩
  • Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat. Symmetry reduction for time Petri net state classes. Science of Computer Programming, Elsevier, 2016, Science of Computer Programming, 132 (Part 2), pp.209 - 225. ⟨10.1016/j.scico.2016.08.008⟩. ⟨hal-01561994⟩
  • Didier Le Botlan, Silvano Dal Zilio, Nouha Abid. A Formal Framework to Specify and Verify Real Time Properties on Critical Systems. International Journal of Critical Computer-Based Systems, Inderscience, 2014, 5 (1/2), pp 4-30. ⟨10.1504/IJCCBS.2014.059593⟩. ⟨hal-00941248⟩
  • Roberto M. Amadio, Silvano Dal Zilio. Resource Control for Synchronous Cooperative Threads. Theoretical Computer Science, Elsevier, 2006, 358, pp.229-254. ⟨hal-00015836⟩
  • Silvano Dal Zilio, Denis Lugiez. XML schema, tree logic and sheaves automata. Applicable Algebra in Engineering, Communication and Computing, Springer Verlag, 2006, 17, pp.337-377. ⟨10.1007/s00200-006-0016-7⟩. ⟨hal-00109288⟩

Conference papers39 documents

  • Nicolas Amat, Silvano Dal Zilio, Thomas Hujsa. Property Directed Reachability for Generalized Petri Nets. Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022, Apr 2022, Munich, Germany. ⟨10.1007/978-3-030-99524-9_28⟩. ⟨hal-03545594⟩
  • Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio. On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets. 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⟩. ⟨hal-03202111⟩
  • Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan. Accelerating the Computation of Dead and Concurrent Places using Reductions. 27th International SPIN Symposium on Model Checking of Software, Jul 2021, Aarhus, Denmark. ⟨10.1007/978-3-030-84629-9_3⟩. ⟨hal-03268388⟩
  • Vincent Mussot, Silvano Dal Zilio, Loic Correnson, Serge Rainjonneau, Yves Bardout, et al.. Formal Approach for the Verification of Onboard Autonomous Functions in Observation Satellites. 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020), Jan 2020, Toulouse, France. ⟨hal-02462058⟩
  • Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias. A New Product Construction for the Diagnosability of Patterns in Time Petri Net. 59th Conference on Decision and Control (CDC) 2020, Dec 2020, Jeju Island (virtual conference), South Korea. ⟨10.1109/CDC42340.2020.9303826⟩. ⟨hal-02989834⟩
  • Silvano Dal Zilio. MCC: a Tool for Unfolding Colored Petri Nets in PNML Format. 41st International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2020, Paris, France. ⟨hal-02511881⟩
  • Elvio Amparore, Bernard Berthomieu, Gianfranco Ciardo, Silvano Dal Zilio, Francesco Gallà, et al.. Presentation of the 9th Edition of the Model Checking Contest. 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⟩. ⟨hal-02094047⟩
  • Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias. A State Class Construction for Computing the Intersection of Time Petri Nets Languages. 17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Aug 2019, Amsterdam, Netherlands. ⟨10.1007/978-3-030-29662-9_5⟩. ⟨hal-02263832⟩
  • Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, et al.. Formal Verification of Complex Robotic Systems on Resource-Constrained Platforms. FormaliSE: 6th International Conference on Formal Methods in Software Engineering, Jun 2018, Gothenburg, Sweden. ⟨hal-01778960⟩
  • Alexandre Albore, Silvano Dal Zilio, Marie de Roquemaurel, Christel Seguin, Pierre Virelizier. Timed Formal Model and Verification of Satellite FDIR in Early Design Phase. 9th European Congress on Embedded Real Time Software and Systems (ERTS 2018), Jan 2018, Toulouse, France. 10p. ⟨hal-01709008⟩
  • Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio. Petri Net Reductions for Counting Markings. International Symposium on Model Checking Software (SPIN 2018), Jun 2018, Malaga, Spain. ⟨10.1007/978-3-319-94111-0_4⟩. ⟨hal-01822078⟩
  • Alexandre Albore, Silvano Dal Zilio, Guillaume Infantes, Christel Seguin, Pierre Virelizier. A Model-Checking Approach to Analyse Temporal Failure Propagation with AltaRica. Model-Based Safety and Assessment. IMBSA 2017, Sep 2017, Trento, Italy. 15p., ⟨10.1007/978-3-319-64119-5_10⟩. ⟨hal-01693391v2⟩
  • Ning Ge, Marc Pantel, Silvano Dal Zilio. Formal Verification of User-Level Real-Time Property Patterns. 11th International Symposium on Theoretical Aspects of Software Engineering (TASE 2017), Sep 2017, Sophia Antipolis, France. 8p. ⟨hal-01589479⟩
  • Pierre-Emmanuel Hladik, Silvano Dal Zilio, Olivier Pasquier, Sébastien Pillement, Bernard Berthomieu. Outillage pour la modélisation, la vérification et la génération d'applications temporisées et embarquées. 15èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Jun 2016, Besançon, France. ⟨hal-01331726⟩
  • Florent Avellaneda, Silvano Dal Zilio, Jean-Baptiste Raclet. Solving Language Equations Using Flanked Automata. ATVA 2016: Automated Technology for Verification and Analysis, Oct 2016, Chiba, Japan. pp.106 - 121, ⟨10.1007/978-3-319-46520-3_7⟩. ⟨hal-01202702v2⟩
  • Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, Félix Ingrand, Anthony Mallet. Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots. 18th International Conference on Formal Engineering Methods (ICFEM 2016), Nov 2016, Tokyo, Japan. ⟨hal-01346080⟩
  • Pierre-Alain Bourdil, Eric Jenn, Silvano Dal Zilio. Building Confidence on Formal Verification Models. Fast Abstracts at International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Sep 2016, Trondheim, Norway. ⟨hal-01369144⟩
  • Silvano Dal Zilio, Bernard Berthomieu. Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus. 1st International Conference on Theoretical Computer Science (TTCS), Aug 2015, Teheran, Iran. pp.90-104, ⟨10.1007/978-3-319-28678-5_7⟩. ⟨hal-01202799⟩
  • Maxime Chéramy, Pierre-Emmanuel Hladik, Anne-Marie Déplanche, Silvano Dal Zilio. Simulation of Real-Time Scheduling Algorithms with Cache Effects. 6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems, Jul 2015, Lund, Sweden. 6p. ⟨hal-01232512⟩
  • Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat. Symmetry reduced state classes for Time Petri nets. 30th Annual ACM Symposium on Applied Computing, Apr 2015, Salamanca, Spain. pp.1751-1758, ⟨10.1145/2695664.2695803⟩. ⟨hal-01275316⟩
  • Silvano Dal Zilio, Lukasz Fronc, Bernard Berthomieu, François Vernadat. Time Petri Nets with Dynamic Firing Dates: Semantics and Applications. 12th International Conference, FORMATS 2014, Sep 2014, Florence, Italy. pp 85-99, ⟨10.1007/978-3-319-10512-3_7⟩. ⟨hal-00984354⟩
  • Bernard Berthomieu, Silvano Dal Zilio, Lukasz Fronc. Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre. 4th International ABZ Conference, Jun 2014, France. pp.110-125. ⟨hal-00967422⟩
  • Nouha Abid, Silvano Dal Zilio. A Verified Approach to Checking Real-Time Patterns on Fiacre Programs. Doctoral Symposium of FM 2012, Aug 2012, Paris, France. ⟨hal-01790120⟩
  • Nouha Abid, Silvano Dal Zilio, Didier Le Botlan. Real-Time Specification Patterns and Tools. 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⟩. ⟨hal-00782649⟩
  • Nawal Guermouche, Silvano Dal Zilio. Towards Timed Requirement Verification for Service Choreographies. 8th IEEE International Conference on Collaborative Computing: Networking, Applications and Worksharing, Oct 2012, Pittsburgh, United States. pp.10. ⟨hal-00578436v4⟩
  • Rodrigo Tacla Saad, Silvano Dal Zilio, Bernard Berthomieu. An Experiment on Parallel Model Checking of a CTL Fragment. 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⟩. ⟨hal-00782354⟩
  • Nouha Abid, Silvano Dal Zilio, Didier Le Botlan. A Verified Approach for Checking Real-Time Specification Patterns. VECoS 2012, 6th International Workshop on Verification and Evaluation of Computer and Communication Systems, Aug 2012, France. pp.11. ⟨hal-00782647v2⟩
  • Rodrigo Tacla Saad, Silvano Dal Zilio, Bernard Berthomieu. Mixed Shared-Distributed Hash Tables Approaches for Parallel State Space Construction. International Symposium on Parallel and Distributed Computing (ISPDC 2011), Jul 2011, Cluj-Napoca, Romania. 8p. ⟨hal-00523188v3⟩
  • Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, Pierre Dissaux, M Filali, et al.. Formal Verification of AADL models with Fiacre and Tina. 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⟩. ⟨hal-00494348⟩
  • Rodrigo Tacla Saad, Silvano Dal Zilio, Bernard Berthomieu. A General Lock-Free Algorithm for Parallel State Space Construction. 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⟩. ⟨hal-00473072v2⟩
  • Silvano Dal Zilio, Nouha Abid. Real-time Extensions for the Fiacre modeling language. MoVep 2010, Summer School on Modelling and Verifying Parallel Processes, Jun 2010, Aachen, Germany. ⟨hal-00494617⟩
  • Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, M Filali, Marc Pantel, et al.. 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. IDM 2010 : journées sur l'Ingénierie Dirigée par les Modèles, Mar 2010, Pau, France. ⟨hal-00492327⟩
  • Rodrigo Tacla Saad, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat. Enumerative Parallel and Distributed State Space Construction. ETR09 - École d'été Temps Réel, Aug 2009, Paris, France. ⟨hal-00494622⟩
  • Rodrigo Tacla Saad, François Vernadat, Bernard Berthomieu, Silvano Dal Zilio. Observation Graph implementation for TINA toolbox. 12th European Workshop on Dependable Computing, EWDC 2009, May 2009, Toulouse, France. 4 p. ⟨hal-00380671⟩
  • Bernard Berthomieu, J.-P Bodeveix, Christelle Chaudet, Silvano Dal Zilio, M Filali, et al.. Formal Verification of AADL Specifications in the Topcased Environment. Reliable Software Technologies - Ada Europe 2009, Jun 2009, Brest, France. 15p., ⟨10.1007/978-3-642-01924-1_15⟩. ⟨hal-01790208⟩
  • Lucia Acciai, Michele Boreale, Silvano Dal Zilio. A Typed Calculus for Querying Distributed XML Documents. 17th Nordic Workshop on Programming Theory, 2005, Copenhagen, Denmark. ⟨hal-00091917⟩
  • Roberto Amadio, Solange Coupet-Grimal, Silvano Dal Zilio, Line Jakubiec. A Functional Scenario for Bytecode Verification of Resource Bounds. Sep 2004, pp.265-279. ⟨hal-00146991⟩
  • Roberto Amadio, Silvano Dal Zilio. Resource Control for Synchronous Cooperative Threads. CONCUR Concurrency Theory, Aug 2004, pp.68-82. ⟨hal-00146983⟩
  • Silvano Dal Zilio. Quiet and Bouncing Objects: Two Migration Abstractions in a Simple Distributed Blue Calculus. SOAP'98 -- 1st International Workshop on Semantics of Objects as Processes, 1998, Aalborg, Denmark. pp.7. ⟨hal-00091895⟩

Other publications1 document

  • Nouha Abid, Silvano Dal Zilio. Real-time Extensions for the Fiacre modeling language. 2010, http://automata.rwth-aachen.de/movep2010/index.php?page=about. ⟨hal-00593958⟩

Preprints, Working Papers, ...7 documents

  • Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet. A formal toolchain for offline and run-time verification of robotics systems: This is an extended version (including the Minnie RMP440 experiment) of a paper currently under review. 2022. ⟨hal-03683044⟩
  • Nicolas Amat, Silvano Dal Zilio, Bernard Berthomieu. A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking. 2021. ⟨hal-03455697⟩
  • Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan. On the Petri Nets with a Single Shared Place and Beyond. 2020. ⟨hal-02992541⟩
  • Thomas Hujsa, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan. Checking marking reachability with the state equation in Petri net subclasses. 2020. ⟨hal-02992521⟩
  • Pierre-Alain Bourdil, Silvano Dal Zilio, Eric Jenn. Integrating Model Checking in an Industrial Verification Process: a Structuring Approach. 2016. ⟨hal-01341701⟩
  • Silvano Dal Zilio, Bernard Berthomieu, Didier Le Botlan. Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina. 2015. ⟨hal-01202741⟩
  • Lucia Acciai, Michele Boreale, Silvano Dal Zilio. A Concurrent Calculus with Atomic Transactions. 2006. ⟨hal-00109264⟩

Reports8 documents

  • Bernard Berthomieu, Jean-Paul Bodeveix, Silvano Dal Zilio, M Filali, Didier Le Botlan, et al.. Real-Time Model Checking Support for AADL. [Research Report] LAAS-CNRS. 2015. ⟨hal-01121605⟩
  • Nouha Abid, Silvano Dal Zilio, Didier Le Botlan. A Real-Time Specification Patterns Language. 2011. ⟨hal-00593965v4⟩
  • Nouha Abid, Silvano Dal Zilio, Didier Le Botlan. Verification of Real-Time Specification Patterns on Time Transition Systems. 2011. ⟨hal-00593963v5⟩
  • Rodrigo Tacla Saad, Silvano Dal Zilio, Bernard Berthomieu. Parallel Model Checking With Lazy Cycle Detection - MCLCD. 2011. ⟨hal-00669752v2⟩
  • Silvano Dal Zilio, Denis Lugiez, Charles Meyssonnier. A Logic You Can Count On. RR-5022, INRIA. 2003. ⟨inria-00071562⟩
  • Silvano Dal Zilio, Denis Lugiez. XML Schema, Tree Logic and Sheaves Automata. RR-4631, INRIA. 2002. ⟨inria-00071954⟩
  • Silvano Dal Zilio. A Bisimulation for the Blue Calculus. RR-3664, INRIA. 1999. ⟨inria-00073008⟩
  • Silvano Dal Zilio. Implicit Polymorphic Type System for the Blue Calculus. RR-3244, INRIA. 1997. ⟨inria-00073445⟩