"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. - Roberto Sebastiani; Stefano Tonetta (CHARME, 2003)

From PSL to NBA: a Modular Symbolic Encoding. - Alessandro Cimatti; Marco Roveri; Simone Semprini; Stefano Tonetta (FMCAD, 2006)

A new hybrid approach for efficient LTL model checking. - Stefano Tonetta (2006)

Boolean Abstraction for Temporal Logic Satisfiability. - Alessandro Cimatti; Marco Roveri; Viktor Schuppan; Stefano Tonetta (CAV, 2007)

Syntactic Optimizations for PSL Verification. - Alessandro Cimatti; Marco Roveri; Stefano Tonetta (TACAS, 2007)

Property-Driven Partitioning for Abstraction Refinement. - Roberto Sebastiani; Stefano Tonetta; Moshe Y. Vardi (TACAS, 2007)

GSTE is partitioned model checking. - Roberto Sebastiani; Eli Singerman; Stefano Tonetta; Moshe Y. Vardi (Formal Methods Syst. Des., 2007)

Loop Summarization Using Abstract Transformers. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (ATVA, 2008)

From Informal Requirements to Property-Driven Formal Validation. - Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta (FMICS, 2008)

Object Models with Temporal Constraints. - Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta (SEFM, 2008)

Symbolic Compilation of PSL. - Alessandro Cimatti; Marco Roveri; Stefano Tonetta (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008)

Requirements Validation for Hybrid Systems. - Alessandro Cimatti; Marco Roveri; Stefano Tonetta (CAV, 2009)

Abstract Model Checking without Computing the Abstraction. - Stefano Tonetta (FM, 2009)

Supporting Requirements Validation: The EuRailCheck Tool. - Roberto Cavada; Alessandro Cimatti; Alessandro Mariotti; Cristian Mattarei; Andrea Micheli; Sergio Mover; Marco Pensallorto; Marco Roveri; Angelo Susi; Stefano Tonetta (ASE, 2009)

Loopfrog: A Static Analyzer for ANSI-C Programs. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (ASE, 2009)

The synergy of precise and fast abstractions for program verification. - Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich (SAC, 2009)

An abstraction refinement approach combining precise and approximated techniques for efficient program verification: abstract for the invited talk. - Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich (SAVCBS, 2009)

Formalization and Validation of Safety-Critical Requirements - Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta (FMA, 2009)

Loopfrog - loop summarization for static analysis. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (WING@ETAPS/IJCAR, 2010)

Model Checking of Hybrid Systems Using Shallow Synchronization. - Lei Bu; Alessandro Cimatti; Xuandong Li; Sergio Mover; Stefano Tonetta (FMOODS/FORTE, 2010)

Formalization and validation of a subset of the European Train Control System. - Angelo Chiappini; Alessandro Cimatti; Luca Macchi; Oscar Rebollo; Marco Roveri; Angelo Susi; Stefano Tonetta; Berardino Vittorini (ICSE (2), 2010)

From Sequential Extended Regular Expressions to NFA with Symbolic Labels. - Alessandro Cimatti; Sergio Mover; Marco Roveri; Stefano Tonetta (CIAA, 2010)

Efficient Scenario Verification for Hybrid Automata. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (CAV, 2011)

HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (EUROMICRO-SEAA, 2011)

Proving and explaining the unfeasibility of message sequence charts for hybrid systems. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (FMCAD, 2011)

OthelloPlay: a plug-in based tool for requirement formalization and validation. - Roberto Cavada; Alessandro Cimatti; Andrea Micheli; Marco Roveri; Angelo Susi; Stefano Tonetta (TOPI@ICSE, 2011)

Symbolic Model Checking and Safety Assessment of Altarica models. - Marco Bozzano; Alessandro Cimatti; Oleg Lisagor; Cristian Mattarei; Sergio Mover; Marco Roveri; Stefano Tonetta (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Formalizing requirements with object models and temporal constraints. - Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta (Softw. Syst. Model., 2011)

Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. - Roberto Sebastiani; Stefano Tonetta; Moshe Y. Vardi (Int. J. Softw. Tools Technol. Transf., 2011)

SMT-Based Verification of Hybrid Systems. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (AAAI, 2012)

A Property-Based Proof System for Contract-Based Design. - Alessandro Cimatti; Stefano Tonetta (EUROMICRO-SEAA, 2012)

A quantifier-free SMT encoding of non-linear hybrid automata. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (FMCAD, 2012)

An abstraction refinement approach combining precise and approximated techniques. - Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich (Int. J. Softw. Tools Technol. Transf., 2012)

Validation of requirements for hybrid systems: A formal approach. - Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta (ACM Trans. Softw. Eng. Methodol., 2012)

A Formal Framework for the Specification, Verification and Synthesis of Diagnosers. - Marco Bozzano; Alessandro Cimatti; Marco Gario; Stefano Tonetta (AAAI (Late-Breaking Developments), 2013)

Time-aware relational abstractions for hybrid systems. - Sergio Mover; Alessandro Cimatti; Ashish Tiwari 001; Stefano Tonetta (EMSOFT, 2013)

Parameter synthesis with IC3. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (FMCAD, 2013)

OCRA: A tool for checking the refinement of temporal contracts. - Alessandro Cimatti; Michele Dorigatti; Stefano Tonetta (ASE, 2013)

SMT-based scenario verification for hybrid systems. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (Formal Methods Syst. Des., 2013)

Loop summarization using state and transition invariants. - Daniel Kroening; Natasha Sharygina; Stefano Tonetta; Aliaksei Tsitovich; Christoph M. Wintersteiger (Formal Methods Syst. Des., 2013)

Formal Safety Assessment via Contract-Based Design. - Marco Bozzano; Alessandro Cimatti; Cristian Mattarei; Stefano Tonetta (ATVA, 2014)

The nuXmv Symbolic Model Checker. - Roberto Cavada; Alessandro Cimatti; Michele Dorigatti; Alberto Griggio; Alessandro Mariotti; Andrea Micheli; Sergio Mover; Marco Roveri; Stefano Tonetta (CAV, 2014)

Verifying LTL Properties of Hybrid Systems with K-Liveness. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (CAV, 2014)

Making Implicit Safety Requirements Explicit - An AUTOSAR Safety Case. - Thomas Arts; Michele Dorigatti; Stefano Tonetta (SAFECOMP, 2014)

Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic. - Marco Bozzano; Alessandro Cimatti; Marco Gario; Stefano Tonetta (TACAS, 2014)

IC3 Modulo Theories via Implicit Predicate Abstraction. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (TACAS, 2014)

Quantifier-free encoding of invariants for hybrid systems. - Alessandro Cimatti; Sergio Mover; Stefano Tonetta (Formal Methods Syst. Des., 2014)

Formal Design and Safety Analysis of AIR6110 Wheel Brake System. - Marco Bozzano; Alessandro Cimatti; Anthony Fernandes Pires; David Jones; Greg Kimberly; T. Petri; R. Robinson; Stefano Tonetta (CAV (1), 2015)

Comparing Different Functional Allocations in Automated Air Traffic Control Design. - Cristian Mattarei; Alessandro Cimatti; Marco Gario; Stefano Tonetta; Kristin Y. Rozier (FMCAD, 2015)

Distributed MILS (D-MILS) Specification, Analysis, Deployment, and Assurance of Distributed Critical Systems. - Harald Rueß; Stefano Tonetta (MILS@HiPEAC, 2015)

Safely Using the AUTOSAR End-to-End Protection Library. - Thomas Arts; Stefano Tonetta (SAFECOMP, 2015)

Combining MILS with Contract-Based Design for Safety and Security Requirements. - Alessandro Cimatti; Rance DeLong; Davide Marcantonio; Stefano Tonetta (SAFECOMP Workshops, 2015)

Parameter Synthesis with IC3 (Informal Presentation). - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (SynCoP, 2015)

HyComp: An SMT-Based Model Checker for Hybrid Systems. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (TACAS, 2015)

Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic. - Marco Bozzano; Alessandro Cimatti; Marco Gario; Stefano Tonetta (Log. Methods Comput. Sci., 2015)

HRELTL: A temporal logic for hybrid systems. - Alessandro Cimatti; Marco Roveri; Stefano Tonetta (Inf. Comput., 2015)

Safety assessment of AltaRica models via symbolic model checking. - Marco Bozzano; Alessandro Cimatti; Oleg Lisagor; Cristian Mattarei; Sergio Mover; Marco Roveri; Stefano Tonetta (Sci. Comput. Program., 2015)

Contracts-refinement proof system for component-based embedded systems. - Alessandro Cimatti; Stefano Tonetta (Sci. Comput. Program., 2015)

A Lazy Approach to Temporal Epistemic Logic Model Checking. - Alessandro Cimatti; Marco Gario; Stefano Tonetta (AAMAS, 2016)

Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations. - Jakub Daniel; Alessandro Cimatti; Alberto Griggio; Stefano Tonetta; Sergio Mover (CAV (1), 2016)

Model Checking at Scale: Automated Air Traffic Control Design Space Exploration. - Marco Gario; Alessandro Cimatti; Cristian Mattarei; Stefano Tonetta; Kristin Yvonne Rozier (CAV (2), 2016)

Model-Based Design of an Energy-System Embedded Controller Using Taste. - Roberto Cavada; Alessandro Cimatti; Luigi Crema; Mattia Roccabruna; Stefano Tonetta (FM, 2016)

Verification of Railway Interlocking - Compositional Approach with OCRA. - Christophe Limbrée; Quentin Cappart; Charles Pecheur; Stefano Tonetta (RSSRail, 2016)

Catalogue of System and Software Properties. - Victor Bos; Harold Bruintjes; Stefano Tonetta (SAFECOMP, 2016)

Tightening a Contract Refinement. - Alessandro Cimatti; Ramiro Demasi; Stefano Tonetta (SEFM, 2016)

Infinite-state invariant checking with IC3 and predicate abstraction. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Stefano Tonetta (Formal Methods Syst. Des., 2016)

From System Specification to Anomaly Detection (and back). - Davide Fauri; Daniel Ricardo dos Santos; Elisa Costante; Jerry den Hartog; Sandro Etalle; Stefano Tonetta (CPS-SPC@CCS, 2017)

Linear-time Temporal Logic with Event Freezing Functions. - Stefano Tonetta (GandALF, 2017)

Formal Specification and Verification of Dynamic Parametrized Architectures. - Alessandro Cimatti; Ivan Stojic; Stefano Tonetta (FM, 2018)

Certifying Proofs for LTL Model Checking. - Alberto Griggio; Marco Roveri; Stefano Tonetta (FMCAD, 2018)

Towards adaptive MILS System: Model- Based Design, Verification and Run-Time Adaptation: Slides. - Alessandro Cimatti; Rance DeLong; Ivan Stojic; Stefano Tonetta (MILS@DSN, 2018)

Tightening the contract refinements of a system architecture. - Alessandro Cimatti; Ramiro Demasi; Stefano Tonetta (Formal Methods Syst. Des., 2018)

Extending nuXmv with Timed Transition Systems and Timed Temporal Properties. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago; Marco Roveri; Stefano Tonetta (CAV (1), 2019)

ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics. - Goran Frehse; Alessandro Abate; Dieky Adzkiya; Anna Becchi; Lei Bu; Alessandro Cimatti; Mirco Giacobbe; Alberto Griggio; Sergio Mover; Muhammad Syifa'ul Mufid; Idriss Riouak; Stefano Tonetta; et al. (ARCH@CPSIoTWeek, 2019)

Assumption-Based Runtime Verification with Partial Observability and Resets. - Alessandro Cimatti; Chun Tian 001; Stefano Tonetta (RV, 2019)

NuRV: A nuXmv Extension for Runtime Verification. - Alessandro Cimatti; Chun Tian 001; Stefano Tonetta (RV, 2019)

Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems. - Alessandro Cimatti; Rance DeLong; Ivan Stojic; Stefano Tonetta (SAFECOMP, 2019)

COMPASS 3.0. - Marco Bozzano; Harold Bruintjes; Alessandro Cimatti; Joost-Pieter Katoen; Thomas Noll 001; Stefano Tonetta (TACAS (1), 2019)

Reactive Synthesis from Extended Bounded Response LTL Specifications. - Alessandro Cimatti; Luca Geatti; Nicola Gigante; Angelo Montanari; Stefano Tonetta (FMCAD, 2020)

Model-Based Safety Analysis of Mode Transitions. - Marco Bozzano; Peter Munk; Markus Schweizer; Stefano Tonetta; Viktória Vozárová (SAFECOMP, 2020)

A Cloud-based Collaboration Platform for Model-based Design of Cyber-Physical Systems. - Peter Gorm Larsen; Hugo Daniel Macedo; John S. Fitzgerald; Holger Pfeifer; Martin Benedikt; Stefano Tonetta; Angelo Marguglio; Sergio Gusmeroli; George Suciu Jr. (SIMULTECH, 2020)

HUBCAP: A Novel Collaborative Approach to Model-Based Design of Cyber-Physical Systems. - Peter Gorm Larsen; Hugo Daniel Macedo; John S. Fitzgerald; Holger Pfeifer; Martin Benedikt; Stefano Tonetta; Angelo Marguglio; Giuseppe Veneziano; Lorenzo Sutton; Sergio Gusmeroli; George Suciu (SIMULTECH (Selected Papers), 2020)

Safe Decomposition of Startup Requirements: Verification and Synthesis. - Alessandro Cimatti; Luca Geatti; Alberto Griggio; Greg Kimberly; Stefano Tonetta (TACAS (1), 2020)

SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago; Marco Roveri; Stefano Tonetta (Inf. Comput., 2020)

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. - Sergio Mover; Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Stefano Tonetta (CAV (1), 2021)

Model-based Analysis Support for Dependable Complex Systems in CHESS. - Alberto Debiasi; Felicien Ihirwe; Pierluigi Pierini; Silvia Mazzini; Stefano Tonetta (MODELSWARD, 2021)

A Proposal for the Classification of Methods for Verification and Validation of Safety, Cybersecurity, and Privacy of Automated Systems. - Jose Luis de la Vara; Thomas Bauer 002; Bernhard Fischer; Mustafa Karaca; Henrique Madeira; Martin Matschnig; Silvia Mazzini; Giann Spilere Nandi; Fabio Patrone; David Pereira; José Proença; Rupert Schlick; et al. (QUATIC, 2021)

Modelling the Component-based Architecture and Safety Contracts of ArmAssist in Papyrus for Robotics. - Jabier Martinez; Alejandra Ruiz 001; Ainara Garzo; Thierry Keller; Ansgar Radermacher; Stefano Tonetta (RoSE@ICSE, 2021)

Assumptions and Guarantees for Composable Models in Papyrus for Robotics. - Jabier Martinez; Alejandra Ruiz 001; Ansgar Radermacher; Stefano Tonetta (RoSE@ICSE, 2021)

Assumption-Based Runtime Verification of Infinite-State Systems. - Alessandro Cimatti; Chun Tian 001; Stefano Tonetta (RV, 2021)

Expressiveness of Extended Bounded Response LTL. - Alessandro Cimatti; Luca Geatti; Nicola Gigante; Angelo Montanari; Stefano Tonetta (GandALF, 2021)

Certifying proofs for SAT-based model checking. - Alberto Griggio; Marco Roveri; Stefano Tonetta (Formal Methods Syst. Des., 2021)

The VALU3S ECSEL project: Verification and validation of automated systems safety and security. - Joseba Andoni Agirre; Leire Etxeberria; Raul Barbosa; Stylianos Basagiannis; Georgios Giantamidis; Thomas Bauer 002; Enrico Ferrari; Mikel Labayen Esnaola; Vanessa Orani; Johnny Öberg; David Pereira; José Proença; et al. (Microprocess. Microsystems, 2021)

A first-order logic characterisation of safety and co-safety languages. - Alessandro Cimatti; Luca Geatti; Nicola Gigante; Angelo Montanari; Stefano Tonetta (FoSSaCS, 2022)

COMPASTA: Extending TASTE with Formal Design and Verification Functionality. - Alberto Bombardelli; Marco Bozzano; Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Massimo Nazaria; Edoardo Nicolodi; Stefano Tonetta (IMBSA, 2022)

A comprehensive framework for the analysis of automotive systems. - Alessandro Cimatti; Sara Corfini; Luca Cristoforetti; Marco Di Natale; Alberto Griggio; Stefano Puri; Stefano Tonetta (MoDELS, 2022)

Asynchronous Composition of Local Interface LTL Properties. - Alberto Bombardelli; Stefano Tonetta (NFM, 2022)

The VMT-LIB Language and Tools. - Alessandro Cimatti; Alberto Griggio; Stefano Tonetta (SMT, 2022)

Searching for Ribbon-Shaped Paths in Fair Transition Systems. - Marco Bozzano; Alessandro Cimatti; Stefano Tonetta; Viktória Vozárová (TACAS (1), 2022)

Diagnosability of fair transition systems. - Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Marco Gario; Stefano Tonetta; Viktória Vozárová (Artif. Intell., 2022)

Verification modulo theories. - Alessandro Cimatti; Alberto Griggio; Sergio Mover; Marco Roveri; Stefano Tonetta (Formal Methods Syst. Des., 2022)

Assumption-based Runtime Verification. - Alessandro Cimatti; Chun Tian 001; Stefano Tonetta (Formal Methods Syst. Des., 2022)

Set-Based Invariants over Polynomial Systems. - Alberto Casagrande; Alessandro Cimatti; Luca Dorigo; Carla Piazza; Stefano Tonetta (CILC, 2023)

Metric Temporal Logic with Resettable Skewed Clocks. - Alberto Bombardelli; Stefano Tonetta (DATE, 2023)

SMT-Based Stability Verification of an Industrial Switched PI Control Systems. - Stylianos Basagiannis; Ludovico Battista; Anna Becchi; Alessandro Cimatti; Georgios Giantamidis; Sergio Mover; Alberto Tacchella; Stefano Tonetta; Vassilios A. Tsachouridis (DSN-W, 2023)

Two formal methodologies of Model-Based Safety Assessment for Fault Tree Analysis. - Isabella Lanzani; Riccardo Scattolini; Enrico Zio; Alessandro Cimatti; Marco Bozzano; Stefano Tonetta (ICSRS, 2023)

Symbolic Model Checking of Relative Safety LTL Properties. - Alberto Bombardelli; Alessandro Cimatti; Stefano Tonetta; Marco Zamboni (iFM, 2023)

Reasoning with Metric Temporal Logic and Resettable Skewed Clocks. - Alberto Bombardelli; Stefano Tonetta (NFM, 2023)

EVA: a Tool for the Compositional Verification of AUTOSAR Models. - Alessandro Cimatti; Luca Cristoforetti; Alberto Griggio; Stefano Tonetta; Sara Corfini; Marco Di Natale; Florian Barrau (TACAS (2), 2023)

Automatic Generation of Scenarios for System-level Simulation-based Verification of Autonomous Driving Systems. - Srajan Goyal; Alberto Griggio; Jacob Kimblad; Stefano Tonetta (FMAS@iFM, 2023)

Asynchronous Composition of LTL Properties over Infinite and Finite Traces. - Alberto Bombardelli; Stefano Tonetta (CoRR, 2023)

GR(1) is equivalent to R(1). - Alessandro Cimatti; Luca Geatti; Nicola Gigante; Angelo Montanari; Stefano Tonetta (Inf. Process. Lett., 2023)

A first-order logic characterization of safety and co-safety languages. - Alessandro Cimatti; Luca Geatti; Nicola Gigante; Angelo Montanari; Stefano Tonetta (Log. Methods Comput. Sci., 2023)

Artifact for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2023)

Supplementary Material for TACAS Submission "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2023)

Artifact for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2023)

Supplementary Material for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2023)

Runtime Verification of Autonomous Systems Utilizing Digital Twins as a Service. - Morten Haahr Kristensen; Alberto Bonizzi; Cláudio Gomes 001; Simon Thrane Hansen; Carlos Ignacio Isasa Martin; Hannes Iven; Eduard Kamburjan; Peter Gorm Larsen; Martin Leucker; Prasad Talasila; Valdemar Trøjgård Tang; Stefano Tonetta; et al. (ACSOS-C, 2024)

Formal Verification of Stability for Parametric affine Switched Systems. - Ludovico Battista; Stefano Tonetta (ADHS, 2024)

Another Look at LTL Modulo Theory over Finite and Infinite Traces. - Alberto Bombardelli; Alessandro Cimatti; Alberto Griggio; Stefano Tonetta (Principles of Verification (1), 2024)

Reconstructing the High-Level Structure of Legacy Code via Software Model Checking: An Experience Report. - Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Stefano Tonetta; Federico Bonafini; Matteo Campidelli; Andrea Zasa (FMICS, 2024)

Unifying Asynchronous Logics for Hyperproperties. - Alberto Bombardelli; Laura Bozzelli; César Sánchez 001; Stefano Tonetta (FSTTCS, 2024)

A Switching Event-Triggered Model Predictive Control for HVAC Systems. - Mojtaba Sharifzadeh; Hani Beirami; Federico Bonafini; Matteo Campidelli; Roberto Cavada; Alessandro Cimatti; Stefano Tonetta (ICINCO (1), 2024)

Towards Formal Design of FDIR Components with AI. - Marco Bozzano; Alessandro Cimatti; Marco Cristoforetti; Alberto Griggio; Piergiorgio Svaizer; Stefano Tonetta (ISoLA (4), 2024)

Towards the Formal Verification of SysML v2 Models. - Vince Molnár; Bence Graics; András Vörös 001; Stefano Tonetta; Luca Cristoforetti; Greg Kimberly; Pamela Dyer; Kristin Giammarco; Manfred Köthe; John Hester; Jamie Smith; Christoph Grimm 001 (MoDELS (Companion), 2024)

Model Checking of Optimal LTL and ASAP Properties. - Davide Bresolin; Filippo Fantinato; Stefano Tonetta (OVERLAY, 2024)

Exploiting Assumptions for Effective Monitoring of Real-Time Properties Under Partial Observability. - Alessandro Cimatti; Thomas Møller Grosen; Kim G. Larsen; Stefano Tonetta; Martin Zimmermann 002 (SEFM, 2024)

Leveraging Contracts for Failure Monitoring and Identification in Automated Driving Systems. - Srajan Goyal; Alberto Griggio; Stefano Tonetta (SEFM, 2024)

Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development. - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (TACAS (2), 2024)

Temporal representation and reasoning in data-intensive systems. - Alexander Artikis; Roberto Posenato; Stefano Tonetta (Inf. Syst., 2024)

Supplementary Material for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2024)

Supplementary Material for "Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development". - Lukas König; Christian Heinzemann; Alberto Griggio; Michaela Klauck; Alessandro Cimatti; Franziska Henze; Stefano Tonetta; Stefan Küperkoch; Dennis Fassbender; Michael Hanselmann (Zenodo, 2024)

Fairness, assumptions, and guarantees for extended bounded response LTL+P synthesis. - Alessandro Cimatti; Luca Geatti; Nicola Gigante; Angelo Montanari; Stefano Tonetta (Softw. Syst. Model., 2024)

Extended bounded response LTL: a new safety fragment for efficient reactive synthesis. - Alessandro Cimatti; Luca Geatti; Nicola Gigante; Angelo Montanari; Stefano Tonetta (Formal Methods Syst. Des., 2024)

A Theorem Prover Based Approach for SAT-Based Model Checking Certification. - Giulia Sindoni; Paolo Pasini; Gianpiero Cabodi; Paolo E. Camurati; Alberto Griggio; Marco Palena; Marco Roveri; Stefano Tonetta (CADE, 2025)

Infinite-State Liveness Checking with rlive. - Alessandro Cimatti; Alberto Griggio; Christopher Johannsen; Kristin Yvonne Rozier; Stefano Tonetta (CAV (1), 2025)

A Specification-Driven Approach to Embedded FDIR Code Generation. - Federico Bonafini; Roberto Cavada; Alessandro Cimatti; Guillermo Gomez; Stefano Tonetta (FMICS, 2025)

System-level simulation-based verification of Autonomous Driving Systems with the VIVAS framework and CARLA simulator. - Srajan Goyal; Alberto Griggio; Stefano Tonetta (Sci. Comput. Program., 2025)

Platform-Aware Mission Planning. - Stefan Panjkovic; Alessandro Cimatti; Andrea Micheli; Stefano Tonetta (CoRR, 2025)