2024
Journal articles
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan. On the Complexity of Proving Polyhedral Reductions. Fundamenta Informaticae, 2024, 192 (3-4), pp.363-394. ⟨10.3233/FI-242197⟩. ⟨hal-04712076⟩
Conference papers
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan. Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability. Verification, Model Checking, and Abstract Interpretation. VMCAI 2024, Jan 2024, London, United Kingdom. pp.101-123, ⟨10.1007/978-3-031-50524-9_5⟩. ⟨hal-04375443⟩
2023
Journal articles
Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, Anthony Mallet. A formal toolchain for offline and run-time verification of robotic systems. Robotics and Autonomous Systems, 2023, 159, pp.104301. ⟨10.1016/j.robot.2022.104301⟩. ⟨hal-03683044v2⟩
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan. Leveraging polyhedral reductions for solving Petri net reachability problems. International Journal on Software Tools for Technology Transfer, 2023, 25, pp.95-114. ⟨10.1007/s10009-022-00694-8⟩. ⟨hal-03973463⟩
Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, et al.. From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact). Dagstuhl Artifacts Series, 2023, 9 (1), ⟨10.4230/DARTS.9.1.4⟩. ⟨hal-04254710⟩
Conference papers
Nicolas Amat, Silvano Dal Zilio. SMPT: A Testbed for Reachability Methods in Generalized Petri Nets. 25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.445-453, ⟨10.1007/978-3-031-27481-7_25⟩. ⟨hal-04007410⟩
Sebastian Altmeyer, Étienne André, Silvano Dal Zilio, Loïc Fejoz, Michael González Harbour, et al.. From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Invited Paper). 35th Euromicro Conference on Real-Time Systems (ECRTS 2023), Jul 2023, Vienne, Austria. ⟨10.4230/LIPIcs.ECRTS.2023.19⟩. ⟨hal-04654624⟩
Nicolas Amat, Silvano Dal Zilio, Didier Le Botlan. Automated Polyhedral Abstraction Proving. 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⟩. ⟨hal-04115006⟩
Other documents
Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan. Polyhedral Reductions for Petri nets. Modélisation des Systèmes Réactifs (MSR'23), Nov 2023, Toulouse, France. , 2023. ⟨hal-04355257⟩
2022
Journal articles
Nicolas Amat, Bernard Berthomieu, Silvano Dal Zilio. A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking. Fundamenta Informaticae, 2022, 187 (2-4), pp.103-138. ⟨10.3233/FI-222134⟩. ⟨hal-03455697v2⟩
Conference papers
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⟩
2021
Journal articles
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, 2021, 206, pp.102624. ⟨10.1016/j.scico.2021.102624⟩. ⟨hal-03187896⟩
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, 2021, 181, pp.111033. ⟨10.1016/j.jss.2021.111033⟩. ⟨hal-03017661v4⟩
Conference papers
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⟩
2020
Journal articles
Bernard Berthomieu, Didier Le Botlan, Silvano Dal Zilio. Counting Petri net markings from reduction equations. International Journal on Software Tools for Technology Transfer, 2020, 22, pp.163-181. ⟨10.1007/s10009-019-00519-1⟩. ⟨hal-02125337⟩
Conference papers
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⟩
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⟩
Éric Lubat, Silvano Dal Zilio. A Short Overview on Diagnosability of Patterns in Timed Petri Net. 14th Summer School on Modelling and Verification of Parallel Processes (MOVEP 2020), Jun 2020, (on line), France. ⟨hal-02899522⟩
É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⟩
Preprints, Working Papers, ...
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⟩
2019
Conference papers
É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⟩
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⟩
Other documents
Mohammed Foughali, Silvano Dal Zilio, Félix Ingrand. On the Semantics of the GenoM3 Framework. Rapport LAAS n° 19036. 2019. ⟨hal-01992470⟩
2018
Conference papers
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⟩
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⟩
Other documents
Rafael Scarduelli, Pierre-Alain Bourdil, Silvano Dal Zilio, Didier Le Botlan. Time-accurate Middleware for the Virtualization of Communication Protocols. Rapport LAAS n° 18126. 2018, 48p. ⟨hal-01793367⟩
2017
Conference papers
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⟩
2016
Journal articles
Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat. Symmetry reduction for time Petri net state classes. Science of Computer Programming, 2016, Science of Computer Programming, 132 (Part 2), pp.209 - 225. ⟨10.1016/j.scico.2016.08.008⟩. ⟨hal-01561994⟩
Conference papers
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⟩
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⟩
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⟩
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⟩
Preprints, Working Papers, ...
Pierre-Alain Bourdil, Silvano Dal Zilio, Eric Jenn. Integrating Model Checking in an Industrial Verification Process: a Structuring Approach. 2016. ⟨hal-01341701⟩
2015
Conference papers
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⟩
Reports
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⟩
Preprints, Working Papers, ...
Silvano Dal Zilio, Bernard Berthomieu, Didier Le Botlan. Latency Analysis of an Aerial Video Tracking System Using Fiacre and Tina. 2015. ⟨hal-01202741⟩
2014
Journal articles
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, 2014, 5 (1/2), pp 4-30. ⟨10.1504/IJCCBS.2014.059593⟩. ⟨hal-00941248⟩
Conference papers
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⟩
Other documents
Pierre-Alain Bourdil, Bernard Berthomieu, Silvano Dal Zilio, François Vernadat. Réduction par symétrie du graphe des classes d'états des Réseaux de Petri Temporels. Rapport LAAS n° 14405. Formalisation des activités concurrentes 2014. 2014. ⟨hal-01949504⟩