Alessandro Cimatti
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
177
Venues
43
Active years
1992–2026
Best venue rank
A*
Where they publish
- A*CAV29 papers
- ATACAS21 papers
- BFMCAD18 papers
- A*AAAI15 papers
- BATVA8 papers
- BSAFECOMP7 papers
- AECAI6 papers
- BSEFM6 papers
- ACADE6 papers
- A*IJCAI5 papers
- CISoLA4 papers
- BFM4 papers
- CFMICS3 papers
- CTIME3 papers
- BRV3 papers
- BVMCAI3 papers
- ASAT3 papers
- CDX2 papers
- AMODELS2 papers
- ADATE2 papers
- A*ICSE2 papers
- CFORTE2 papers
- A*DAC2 papers
- BLPAR2 papers
- AIJCAR1 paper
- A*ICAPS1 paper
- A*KR1 paper
- BCPAIOR1 paper
- CICINCO1 paper
- ADSN1 paper
- BIFM1 paper
- BFOSSACS1 paper
- BLPNMR1 paper
- BCONCUR1 paper
- NationalSYNASC1 paper
- Journal PublishedEMSOFT1 paper
- BICECCS1 paper
- ACP1 paper
- CETFA1 paper
- CMEMOCODE1 paper
- ARTSS1 paper
- AustralasianAISC1 paper
- CLOPSTR1 paper
Papers
177 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | IJCAR | Verification of Configurable SRA Systems. | Alessandro Cimatti, Alberto Griggio, Christian Lidstrm, Gianluca Redondi, Dylan Trenti |
| 2026 | SAFECOMP | Diagnosis of Runtime Property Violations. | Marco Bozzano, Alessandro Cimatti, Alberto Sambrotta, Stefano Tonetta |
| 2025 | CAV | Automated Parameterized Verification of a Railway Protection System with Dafny. | Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Christian Lidstrm, Gianluca Redondi, Giuseppe Scaglione, Matteo Tessi, Dylan Trenti |
| 2025 | CAV | Infinite-State Liveness Checking with rlive. | Alessandro Cimatti, Alberto Griggio, Christopher Johannsen, Kristin Yvonne Rozier, Stefano Tonetta |
| 2025 | FMICS | A Specification-Driven Approach to Embedded FDIR Code Generation. | Federico Bonafini, Roberto Cavada, Alessandro Cimatti, Guillermo Gomez, Stefano Tonetta |
| 2025 | ICAPS | Platform-Aware Mission Planning. | Stefan Panjkovic, Alessandro Cimatti, Andrea Micheli, Stefano Tonetta |
| 2025 | KR | Generalizing Platform-Aware Mission Planning for Infinite-State Timed Transition Systems. | Stefan Panjkovic, Alessandro Cimatti, Andrea Micheli, Stefano Tonetta |
| 2024 | CAV | Testing the Migration from Analog to Software-Based Railway Interlocking Systems. | Anna Becchi, Alessandro Cimatti, Giuseppe Scaglione |
| 2024 | CAV | Avoiding the Shoals - A New Approach to Liveness Checking. | Yechuan Xia, Alessandro Cimatti, Alberto Griggio, Jianwen Li |
| 2024 | CPAIOR | SMT-Based Repair of Disjunctive Temporal Networks with Uncertainty: Strong and Weak Controllability. | Ajdin Sumic, Alessandro Cimatti, Andrea Micheli, Thierry Vidal |
| 2024 | DX | Inferring Sensor Placement Using Critical Pairs and Satisfiability Modulo Theory. | Alexander Diedrich, Ren Heesch, Marco Bozzano, Bjrn Ludwig, Alessandro Cimatti, Oliver Niggemann |
| 2024 | DX | Summary of "A Lazy Approach to Neural Numerical Planning with Control Parameters" (Extended Abstract). | Ren Heesch, Alessandro Cimatti, Jonas Ehrhardt, Alexander Diedrich, Oliver Niggemann |
| 2024 | ECAI | A Lazy Approach to Neural Numerical Planning with Control Parameters. | Ren Heesch, Alessandro Cimatti, Jonas Ehrhardt, Alexander Diedrich, Oliver Niggemann |
| 2024 | FMCAD | Towards Verification Modulo Theories of Asynchronous Systems via Abstraction Refinement. | Gianluca Redondi, Alessandro Cimatti, Alberto Griggio |
| 2024 | FMICS | 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 |
| 2024 | ICINCO | A Switching Event-Triggered Model Predictive Control for HVAC Systems. | Mojtaba Sharifzadeh, Hani Beirami, Federico Bonafini, Matteo Campidelli, Roberto Cavada, Alessandro Cimatti, Stefano Tonetta |
| 2024 | ISoLA | Towards Formal Design of FDIR Components with AI. | Marco Bozzano, Alessandro Cimatti, Marco Cristoforetti, Alberto Griggio, Piergiorgio Svaizer, Stefano Tonetta |
| 2024 | ISoLA | Towards the Formal Analysis of Algorithmic Requirements. | Lorenzo Cappelletti, Roberto Cavada, Alessandro Cimatti, Marco Keppel |
| 2024 | ISoLA | Model-Based Testing of Railway Interlocking Systems. | Alessandro Cimatti, Shaker Khandaker, Fitsum Meshesha Kifetew, Lorenzo Leone, Davide Prandi, Giuseppe Scaglione, Angelo Susi, Orazio Turboli |
| 2024 | SEFM | Exploiting Assumptions for Effective Monitoring of Real-Time Properties Under Partial Observability. | Alessandro Cimatti, Thomas Mller Grosen, Kim G. Larsen, Stefano Tonetta, Martin Zimmermann |
| 2024 | TACAS | Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development. | Lukas Knig, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Kperkoch, Dennis Fassbender, Michael Hanselmann |
| 2024 | TIME | Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning. | Ajdin Sumic, Thierry Vidal, Andrea Micheli, Alessandro Cimatti |
| 2023 | CAV | Searching for i-Good Lemmas to Accelerate Safety Model Checking. | Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, Geguang Pu |
| 2023 | DSN | 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 |
| 2023 | IFM | Symbolic Model Checking of Relative Safety LTL Properties. | Alberto Bombardelli, Alessandro Cimatti, Stefano Tonetta, Marco Zamboni |
| 2023 | TACAS | 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 |
| 2022 | AAAI | Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping. | Stefan Panjkovic, Andrea Micheli, Alessandro Cimatti |
| 2022 | ATVA | Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. | Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani |
| 2022 | ATVA | Verification of SMT Systems with Quantifiers. | Alessandro Cimatti, Alberto Griggio, Gianluca Redondi |
| 2022 | CAV | Abstraction Modulo Stability for Reverse Engineering. | Anna Becchi, Alessandro Cimatti |
| 2022 | FOSSACS | A first-order logic characterisation of safety and co-safety languages. | Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta |
| 2022 | LPNMR | Analysis of Cyclic Fault Propagation via ASP. | Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jons, Greg Kimberly |
| 2022 | MODELS | A comprehensive framework for the analysis of automotive systems. | Alessandro Cimatti, Sara Corfini, Luca Cristoforetti, Marco Di Natale, Alberto Griggio, Stefano Puri, Stefano Tonetta |
| 2022 | SEFM | A Formal IDE for Railways: Research Challenges. | Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Angelo Susi |
| 2022 | TACAS | NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems. | Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Andrea Ferrando, Lorenzo Pilati, Giuseppe Scaglione, Alberto Tacchella, Marco Zamboni |
| 2022 | TACAS | Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation. | Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jons |
| 2022 | TACAS | Searching for Ribbon-Shaped Paths in Fair Transition Systems. | Marco Bozzano, Alessandro Cimatti, Stefano Tonetta, Viktria Vozrov |
| 2021 | ATVA | Automatic Discovery of Fair Paths in Infinite-State Transition Systems. | Alessandro Cimatti, Alberto Griggio, Enrico Magnago |
| 2021 | CADE | Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. | Alessandro Cimatti, Alberto Griggio, Gianluca Redondi |
| 2021 | CAV | Efficient SMT-Based Analysis of Failure Propagation. | Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jons, Greg Kimberly |
| 2021 | CAV | Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. | Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Stefano Tonetta |
| 2021 | CONCUR | SMT-Based Model Checking of Max-Plus Linear Systems. | Muhammad Syifa'ul Mufid, Andrea Micheli, Alessandro Abate, Alessandro Cimatti |
| 2021 | RV | Assumption-Based Runtime Verification of Infinite-State Systems. | Alessandro Cimatti, Chun Tian, Stefano Tonetta |
| 2021 | SEFM | Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis. | Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta |
| 2021 | TIME | Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans. | Michael Cashmore, Alessandro Cimatti, Daniele Magazzeni, Andrea Micheli, Parisa Zehtabi |
| 2021 | VMCAI | Proving the Existence of Fair Paths in Infinite-State Systems. | Alessandro Cimatti, Alberto Griggio, Enrico Magnago |
| 2020 | AAAI | Temporal Planning with Intermediate Conditions and Effects. | Alessandro Valentini, Andrea Micheli, Alessandro Cimatti |
| 2020 | FMCAD | Reactive Synthesis from Extended Bounded Response LTL Specifications. | Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta |
| 2020 | ISoLA | A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System. | Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Giuseppe Scaglione, Angelo Susi, Alberto Tacchella, Matteo Tessi |
| 2020 | SEFM | Synthesis of P-Stable Abstractions. | Anna Becchi, Alessandro Cimatti, Enea Zaffanella |
| 2020 | TACAS | Safe Decomposition of Startup Requirements: Verification and Synthesis. | Alessandro Cimatti, Luca Geatti, Alberto Griggio, Greg Kimberly, Stefano Tonetta |
| 2019 | AAAI | Robustness Envelopes for Temporal Plans. | Michael Cashmore, Alessandro Cimatti, Daniele Magazzeni, Andrea Micheli, Parisa Zehtabi |
| 2019 | CAV | Extending nuXmv with Timed Transition Systems and Timed Temporal Properties. | Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, Stefano Tonetta |
| 2019 | RV | Assumption-Based Runtime Verification with Partial Observability and Resets. | Alessandro Cimatti, Chun Tian, Stefano Tonetta |
| 2019 | RV | NuRV: A nuXmv Extension for Runtime Verification. | Alessandro Cimatti, Chun Tian, Stefano Tonetta |
| 2019 | SAFECOMP | Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems. | Alessandro Cimatti, Rance DeLong, Ivan Stojic, Stefano Tonetta |
| 2019 | TACAS | COMPASS 3.0. | Marco Bozzano, Harold Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta |
| 2018 | FM | Formal Specification and Verification of Dynamic Parametrized Architectures. | Alessandro Cimatti, Ivan Stojic, Stefano Tonetta |
| 2018 | FMCAD | Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks. | Roberto Cavada, Alessandro Cimatti, Sergio Mover, Mirko Sessa, Giuseppe Cadavero, Giuseppe Scaglione |
| 2018 | SAT | Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2018 | SYNASC | Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2017 | AAAI | Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic. | Alessandro Cimatti, Andrea Micheli, Marco Roveri |
| 2017 | CADE | SC-square: when Satisfiability Checking and Symbolic Computation join forces. | Erika brahm, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler |
| 2017 | CADE | Satisfiability Modulo Transcendental Functions via Incremental Linearization. | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2017 | FMCAD | SMT-based analysis of switching multi-domain linear Kirchhoff networks. | Alessandro Cimatti, Sergio Mover, Mirko Sessa |
| 2017 | TACAS | Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. | Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani |
| 2016 | AAAI | Automated Verification and Tightening of Failure Propagation Models. | Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Gianni Zampedri |
| 2016 | AAAI | Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies. | Alessandro Cimatti, Andrea Micheli, Marco Roveri |
| 2016 | CAV | Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations. | Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, Sergio Mover |
| 2016 | CAV | Model Checking at Scale: Automated Air Traffic Control Design Space Exploration. | Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, Kristin Yvonne Rozier |
| 2016 | DATE | Verilog2SMV: A tool for word-level verification. | Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani |
| 2016 | FM | Model-Based Design of an Energy-System Embedded Controller Using Taste. | Roberto Cavada, Alessandro Cimatti, Luigi Crema, Mattia Roccabruna, Stefano Tonetta |
| 2016 | FM | From Electrical Switched Networks to Hybrid Automata. | Alessandro Cimatti, Sergio Mover, Mirko Sessa |
| 2016 | IJCAI | Automated Synthesis of Timed Failure Propagation Graphs. | Benjamin Bittner, Marco Bozzano, Alessandro Cimatti |
| 2016 | SEFM | Tightening a Contract Refinement. | Alessandro Cimatti, Ramiro Demasi, Stefano Tonetta |
| 2016 | TACAS | The xSAP Safety Analysis Platform. | Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli, Gianni Zampedri |
| 2015 | AAAI | SMT-Based Validation of Timed Failure Propagation Graphs. | Marco Bozzano, Alessandro Cimatti, Marco Gario, Andrea Micheli |
| 2015 | AAAI | Strong Temporal Planning with Uncontrollable Durations: A State-Space Approach. | Alessandro Cimatti, Andrea Micheli, Marco Roveri |
| 2015 | ATVA | Formal Verification of Infinite-State BIP Models. | Simon Bliudze, Alessandro Cimatti, Mohamad Jaber, Sergio Mover, Marco Roveri, Wajeb Saab, Qiang Wang |
| 2015 | CAV | Efficient Anytime Techniques for Model-Based Safety Analysis. | Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Cristian Mattarei |
| 2015 | CAV | 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 |
| 2015 | FMCAD | Comparing Different Functional Allocations in Automated Air Traffic Control Design. | Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, Kristin Y. Rozier |
| 2015 | SAFECOMP | Combining MILS with Contract-Based Design for Safety and Security Requirements. | Alessandro Cimatti, Rance DeLong, Davide Marcantonio, Stefano Tonetta |
| 2015 | TACAS | HyComp: An SMT-Based Model Checker for Hybrid Systems. | Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
| 2014 | AAAI | Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty. | Alessandro Cimatti, Luke Hunsberger, Andrea Micheli, Marco Roveri |
| 2014 | ATVA | Formal Safety Assessment via Contract-Based Design. | Marco Bozzano, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta |
| 2014 | CAV | The nuXmv Symbolic Model Checker. | Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta |
| 2014 | CAV | Verifying LTL Properties of Hybrid Systems with K-Liveness. | Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
| 2014 | FMCAD | Towards Pareto-optimal parameter synthesis for monotonic cost functions. | Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario, Alberto Griggio |
| 2014 | TACAS | Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic. | Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta |
| 2014 | TACAS | IC3 Modulo Theories via Implicit Predicate Abstraction. | Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
| 2014 | TIME | Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation. | Alessandro Cimatti, Luke Hunsberger, Andrea Micheli, Roberto Posenato, Marco Roveri |
| 2013 | AAAI | A Formal Framework for the Specification, Verification and Synthesis of Diagnosers. | Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta |
| 2013 | AAAI | Timelines with Temporal Uncertainty. | Alessandro Cimatti, Andrea Micheli, Marco Roveri |
| 2013 | ATVA | SMT-Based Software Model Checking - Explicit Scheduler, Symbolic Threads. | Alessandro Cimatti |
| 2013 | EMSOFT | Time-aware relational abstractions for hybrid systems. | Sergio Mover, Alessandro Cimatti, Ashish Tiwari, Stefano Tonetta |
| 2013 | FMCAD | Parameter synthesis with IC3. | Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta |
| 2013 | ICECCS | Automated Analysis of Reliability Architectures. | Marco Bozzano, Alessandro Cimatti, Cristian Mattarei |
| 2013 | SAT | A Modular Approach to MaxSAT Modulo Theories. | Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani |
| 2013 | TACAS | The MathSAT5 SMT Solver. | Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani |
| 2012 | AAAI | Symbolic Synthesis of Observability Requirements for Diagnosability. | Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Xavier Olive |
| 2012 | AAAI | Solving Temporal Problems Using SMT: Weak Controllability. | Alessandro Cimatti, Andrea Micheli, Marco Roveri |
| 2012 | AAAI | SMT-Based Verification of Hybrid Systems. | Alessandro Cimatti, Sergio Mover, Stefano Tonetta |
| 2012 | CAV | Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System. | Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, Tiziana Rizzo, Marco Roveri, Angela Sanseviero, Andrei Tchaltsev |
| 2012 | CAV | Software Model Checking via IC3. | Alessandro Cimatti, Alberto Griggio |
| 2012 | CP | Solving Temporal Problems Using SMT: Strong Controllability. | Alessandro Cimatti, Andrea Micheli, Marco Roveri |
| 2012 | FMCAD | Application of SMT solvers to hybrid system verification. | Alessandro Cimatti |
| 2012 | FMCAD | A quantifier-free SMT encoding of non-linear hybrid automata. | Alessandro Cimatti, Sergio Mover, Stefano Tonetta |
| 2012 | FMCAD | Verification of parametric system designs. | Alessandro Cimatti, Iman Narasamdya, Marco Roveri |
| 2011 | CAV | Kratos - A Software Model Checker for SystemC. | Alessandro Cimatti, Alberto Griggio, Andrea Micheli, Iman Narasamdya, Marco Roveri |
| 2011 | CAV | Efficient Scenario Verification for Hybrid Automata. | Alessandro Cimatti, Sergio Mover, Stefano Tonetta |
| 2011 | FMCAD | Proving and explaining the unfeasibility of message sequence charts for hybrid systems. | Alessandro Cimatti, Sergio Mover, Stefano Tonetta |
| 2011 | IJCAI | A Comprehensive Approach to On-Board Autonomy Verification and Validation. | Marco Bozzano, Alessandro Cimatti, Marco Roveri, Andrei Tchaltsev |
| 2011 | ICSE | OthelloPlay: a plug-in based tool for requirement formalization and validation. | Roberto Cavada, Alessandro Cimatti, Andrea Micheli, Marco Roveri, Angelo Susi, Stefano Tonetta |
| 2011 | TACAS | Boosting Lazy Abstraction for SystemC with Partial Order Reduction. | Alessandro Cimatti, Iman Narasamdya, Marco Roveri |
| 2010 | CAV | RATSY - A New Requirements Analysis Tool with Synthesis. | Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Knighofer, Marco Roveri, Viktor Schuppan, Richard Seeber |
| 2010 | CAV | A Model Checker for AADL. | Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer |
| 2010 | DATE | Tighter integration of BDDs and SMT for Predicate Abstraction. | Alessandro Cimatti, Anders Franzn, Alberto Griggio, Krishnamani Kalyanasundaram, Marco Roveri |
| 2010 | ETFA | Parametric analysis of distributed firm real-time systems: A case study. | Thi Thieu Hoa Le, Luigi Palopoli, Roberto Passerone, Yusi Ramadian, Alessandro Cimatti |
| 2010 | FMCAD | Verifying SystemC: A software model checking approach. | Alessandro Cimatti, Andrea Micheli, Iman Narasamdya, Marco Roveri |
| 2010 | FMCAD | Applying SMT in symbolic execution of microcode. | Anders Franzn, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev |
| 2010 | FORTE | Model Checking of Hybrid Systems Using Shallow Synchronization. | Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta |
| 2010 | ICSE | 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 |
| 2010 | TACAS | Satisfiability Modulo the Theory of Costs: Foundations and Applications. | Alessandro Cimatti, Anders Franzn, Alberto Griggio, Roberto Sebastiani, Cristian Stenico |
| 2009 | CADE | Interpolant Generation for UTVPI. | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
| 2009 | CAV | Requirements Validation for Hybrid Systems. | Alessandro Cimatti, Marco Roveri, Stefano Tonetta |
| 2009 | FMCAD | Software model checking via large-block encoding. | Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani |
| 2009 | FMCAD | Structure-aware computation of predicate abstraction. | Alessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri |
| 2009 | MEMOCODE | Codesign of dependable systems: A component-based modeling language. | Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll |
| 2009 | MODELS | Model-Based Codesign of Critical Embedded Systems. | Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri |
| 2009 | SAFECOMP | The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. | Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri |
| 2008 | CAV | The MathSAT 4SMT Solver. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Roberto Sebastiani |
| 2008 | FMICS | From Informal Requirements to Property-Driven Formal Validation. | Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta |
| 2008 | RTSS | Symbolic Computation of Schedulability Regions Using Parametric Timed Automata. | Alessandro Cimatti, Luigi Palopoli, Yusi Ramadian |
| 2008 | SEFM | Object Models with Temporal Constraints. | Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta |
| 2008 | TACAS | Efficient Interpolant Generation in Satisfiability Modulo Theories. | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
| 2008 | VMCAI | Diagnostic Information for Realizability. | Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Andrei Tchaltsev |
| 2007 | ATVA | Symbolic Fault Tree Analysis for Reactive Systems. | Marco Bozzano, Alessandro Cimatti, Francesco Tapparo |
| 2007 | ATVA | Verifying Heap-Manipulating Programs in an SMT Framework. | Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti |
| 2007 | CAV | A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani |
| 2007 | CAV | Boolean Abstraction for Temporal Logic Satisfiability. | Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta |
| 2007 | FMCAD | Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. | Roberto Cavada, Alessandro Cimatti, Anders Franzn, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar |
| 2007 | SAT | A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
| 2007 | TACAS | Syntactic Optimizations for PSL Verification. | Alessandro Cimatti, Marco Roveri, Stefano Tonetta |
| 2006 | DAC | Formal analysis of hardware requirements. | Ingo Pill, Simone Semprini, Roberto Cavada, Marco Roveri, Roderick Bloem, Alessandro Cimatti |
| 2006 | ECAI | Stong Cyclic Planning Under Partial Observability. | Piergiorgio Bertoli, Alessandro Cimatti, Marco Pistore |
| 2006 | FMCAD | From PSL to NBA: a Modular Symbolic Encoding. | Alessandro Cimatti, Marco Roveri, Simone Semprini, Stefano Tonetta |
| 2006 | LPAR | Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Roberto Sebastiani |
| 2006 | LPAR | To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani |
| 2005 | CADE | The MathSAT 3 System. | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani |
| 2005 | CAV | Efficient Satisfiability Modulo Theories via Delayed Theory Combination. | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani |
| 2005 | TACAS | An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani |
| 2004 | ECAI | Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains. | Piergiorgio Bertoli, Alessandro Cimatti, Paolo Traverso |
| 2004 | ECAI | Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems. | Floris Roelofsen, Luciano Serafini, Alessandro Cimatti |
| 2004 | FMCAD | Bounded Verification of Past LTL. | Alessandro Cimatti, Marco Roveri, Daniel Sheridan |
| 2003 | IJCAI | Formal Verification of Diagnosability via Symbolic Model Checking. | Alessandro Cimatti, Charles Pecheur, Roberto Cavada |
| 2003 | TACAS | Bounded Model Checking for Past LTL. | Marco Benedetti, Alessandro Cimatti |
| 2002 | AISC | Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. | Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
| 2002 | CADE | A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. | Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
| 2002 | CAV | NuSMV 2: An OpenSource Tool for Symbolic Model Checking. | Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella |
| 2002 | ECAI | Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking. | Piergiorgio Bertoli, Alessandro Cimatti, John K. Slaney, Sylvie Thibaux |
| 2002 | FORTE | Bounded Model Checking for Timed Systems. | Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
| 2002 | VMCAI | Improving the Encoding of LTL Model Checking into SAT. | Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani |
| 2001 | IJCAI | Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning. | Piergiorgio Bertoli, Alessandro Cimatti, Marco Roveri |
| 2001 | IJCAI | Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking. | Piergiorgio Bertoli, Alessandro Cimatti, Marco Roveri, Paolo Traverso |
| 2001 | TACAS | Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking. | Alessandro Cimatti, Marco Roveri, Piergiorgio Bertoli |
| 1999 | CAV | NUSMV: A New Symbolic Model Verifier. | Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri |
| 1999 | DAC | Symbolic Model Checking Using SAT Procedures instead of BDDs. | Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu |
| 1999 | FM | Formal Specification and Validation of a Vital Communication Protocol. | Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita |
| 1999 | SAFECOMP | Formal Specification and Development of a Safety-Critical Train Management System. | Angelo Chiappini, Alessandro Cimatti, Carmen Porzia, G. Rotondo, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita |
| 1999 | TACAS | Symbolic Model Checking without BDDs. | Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu |
| 1998 | AAAI | Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic Domains. | Alessandro Cimatti, Marco Roveri, Paolo Traverso |
| 1998 | SAFECOMP | A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools. | Piergiorgio Bertoli, Alessandro Cimatti, Fausto Giunchiglia, Paolo Traverso |
| 1998 | SAFECOMP | Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System. | Alessandro Cimatti, Fausto Giunchiglia, Giorgio Mongardi, Dario Romano, Fernando Torielli, Paolo Traverso |
| 1997 | CAV | A Provably Correct Embedded Verifier for the Certification of Safety Critical Software. | Alessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano, Paolo Traverso, Bing Yu |
| 1994 | LOPSTR | Introspective Metatheoretic Reasoning. | Fausto Giunchiglia, Alessandro Cimatti |
| 1992 | ECAI | Beyond the Single Planning Paradigm: Introspective Planning. | Paolo Traverso, Alessandro Cimatti, Luca Spalazzi |