Alessandro Cimatti

324 papers A* 41A 34B 54C 18Misc 3Journal 84Unranked 86
YearRankTypeTitle / Venue / Authors
2026 J jnl
Multiple interdependent Simple Temporal Networks with Uncertainty: A semi-decentralized multi-agent model with shared control of activity durations.
Inf. Comput.
Ajdin Sumic, Thierry Vidal, Andrea Micheli, Alessandro Cimatti
2025 C conf
A Specification-Driven Approach to Embedded FDIR Code Generation.
FMICS
Federico Bonafini, Roberto Cavada, Alessandro Cimatti, Guillermo Gomez, Stefano Tonetta
2025 — conf
AI for industry at FBK.
Ital-IA
Alessandro Cimatti, Fabio Antonelli, Luisa Bentivogli, Marco Cristoforetti, Andrea Micheli, Fabio Poiesi, Fabio Remondino, Angelo Susi, Stefano Tonetta
2025 J jnl
Abstraction Modulo Stability.
Formal Methods Syst. Des.
Anna Becchi, Alessandro Cimatti
2025 — conf
Automated Parameterized Verification of a Railway Protection System with Dafny.
CAV (4)
Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Christian Lidström, Gianluca Redondi, Giuseppe Scaglione, Matteo Tessi, Dylan Trenti
2025 J jnl
Automatic digitalization of railway interlocking systems engineering drawings based on hybrid machine learning methods.
Expert Syst. Appl.
Stéfano Frizzo Stefenon, Marco Cristoforetti, Alessandro Cimatti
2025 J jnl
Conditional diffusion to enhance performance of object detection in unbalanced data engineering drawings.
Neural Comput. Appl.
Stéfano Frizzo Stefenon, Marco Cristoforetti, Alessandro Cimatti
2025 — conf
Formal Analysis of a Railway Signaling Block Designed in AIDA.
RSSRail
Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Christian Lidström, Gianluca Redondi, Matteo Tessi, Dylan Trenti
2025 J jnl
Formal methods in industrial critical systems.
Int. J. Softw. Tools Technol. Transf.
Alessandro Cimatti, Laura Titolo
2025 A* conf
Generalizing Platform-Aware Mission Planning for Infinite-State Timed Transition Systems.
KR
Stefan Panjkovic, Alessandro Cimatti, Andrea Micheli, Stefano Tonetta
2025 — conf
Infinite-State Liveness Checking with rlive.
CAV (1)
Alessandro Cimatti, Alberto Griggio, Christopher Johannsen, Kristin Yvonne Rozier, Stefano Tonetta
2025 J jnl
Platform-Aware Mission Planning.
CoRR
Stefan Panjkovic, Alessandro Cimatti, Andrea Micheli, Stefano Tonetta
2025 — conf
Towards a Unifying View of Fault Propagation Analyses and Notations.
IMBSA
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Fajar Haifani
2024 A conf
A Lazy Approach to Neural Numerical Planning with Control Parameters.
ECAI
René Heesch, Alessandro Cimatti, Jonas Ehrhardt, Alexander Diedrich, Oliver Niggemann
2024 C conf
A Switching Event-Triggered Model Predictive Control for HVAC Systems.
ICINCO (1)
Mojtaba Sharifzadeh, Hani Beirami, Federico Bonafini, Matteo Campidelli, Roberto Cavada, Alessandro Cimatti, Stefano Tonetta
2024 — conf
Another Look at LTL Modulo Theory over Finite and Infinite Traces.
Principles of Verification (1)
Alberto Bombardelli, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta
2024 — conf
Avoiding the Shoals - A New Approach to Liveness Checking.
CAV (1)
Yechuan Xia, Alessandro Cimatti, Alberto Griggio, Jianwen Li
2024 B conf
Exploiting Assumptions for Effective Monitoring of Real-Time Properties Under Partial Observability.
SEFM
Alessandro Cimatti, Thomas Møller Grosen, Kim G. Larsen, Stefano Tonetta, Martin Zimmermann
2024 J jnl
Exploiting Assumptions for Effective Monitoring of Real-Time Properties under Partial Observability.
CoRR
Alessandro Cimatti, Thomas Møller Grosen, Kim G. Larsen, Stefano Tonetta, Martin Zimmermann
2024 J jnl
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis.
Formal Methods Syst. Des.
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2024 J jnl
Fairness, assumptions, and guarantees for extended bounded response LTL+P synthesis.
Softw. Syst. Model.
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2024 J jnl
Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis (Dagstuhl Seminar 24031).
Dagstuhl Reports
Alessandro Cimatti, Ingo Pill, Alexander Diedrich
2024 C conf
Inferring Sensor Placement Using Critical Pairs and Satisfiability Modulo Theory.
DX
Alexander Diedrich, René Heesch, Marco Bozzano, Björn Ludwig, Alessandro Cimatti, Oliver Niggemann
2024 C conf
Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning.
TIME
Ajdin Sumic, Thierry Vidal, Andrea Micheli, Alessandro Cimatti
2024 J jnl
Invariant Checking for SMT-Based Systems with Quantifiers.
ACM Trans. Comput. Log.
Gianluca Redondi, Alessandro Cimatti, Alberto Griggio, Kenneth L. McMillan
2024 J jnl
Invariant Checking for SMT-based Systems with Quantifiers.
CoRR
Gianluca Redondi, Alessandro Cimatti, Alberto Griggio, Kenneth L. McMillan
2024 — conf
Model-Based Testing of Railway Interlocking Systems.
ISoLA (5)
Alessandro Cimatti, Shaker Khandaker, Fitsum Meshesha Kifetew, Lorenzo Leone, Davide Prandi, Giuseppe Scaglione, Angelo Susi, Orazio Turboli
2024 J jnl
Opportunistic (Re)planning for Long-Term Deep-Ocean Inspection: An Autonomous Underwater Architecture.
IEEE Robotics Autom. Mag.
Elisa Tosello, Paolo Bonel, Alberto Buranello, Marco Carraro, Alessandro Cimatti, Lorenzo Granelli, Stefan Panjkovic, Andrea Micheli
2024 J jnl
P-stable abstractions of hybrid systems.
Softw. Syst. Model.
Anna Becchi, Alessandro Cimatti, Enea Zaffanella
2024 C conf
Reconstructing the High-Level Structure of Legacy Code via Software Model Checking: An Experience Report.
FMICS
Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, Federico Bonafini, Matteo Campidelli, Andrea Zasa
2024 — conf
SMT-Based Repair of Disjunctive Temporal Networks with Uncertainty: Strong and Weak Controllability.
CPAIOR (2)
Ajdin Sumic, Alessandro Cimatti, Andrea Micheli, Thierry Vidal
2024 C conf
Summary of "A Lazy Approach to Neural Numerical Planning with Control Parameters" (Extended Abstract).
DX
René Heesch, Alessandro Cimatti, Jonas Ehrhardt, Alexander Diedrich, Oliver Niggemann
2024 — conf
Testing the Migration from Analog to Software-Based Railway Interlocking Systems.
CAV (2)
Anna Becchi, Alessandro Cimatti, Giuseppe Scaglione
2024 — conf
Towards Formal Design of FDIR Components with AI.
ISoLA (4)
Marco Bozzano, Alessandro Cimatti, Marco Cristoforetti, Alberto Griggio, Piergiorgio Svaizer, Stefano Tonetta
2024 — conf
Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development.
TACAS (2)
Lukas König, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze, Stefano Tonetta, Stefan Küperkoch, Dennis Fassbender, Michael Hanselmann
2024 B conf
Towards Verification Modulo Theories of Asynchronous Systems via Abstraction Refinement.
FMCAD
Gianluca Redondi, Alessandro Cimatti, Alberto Griggio
2024 — conf
Towards the Formal Analysis of Algorithmic Requirements.
ISoLA (3)
Lorenzo Cappelletti, Roberto Cavada, Alessandro Cimatti, Marco Keppel
2024 J jnl
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking.
CoRR
Alessandro Cimatti, Alberto Griggio, Gianluca Redondi
2023 J jnl
A first-order logic characterization of safety and co-safety languages.
Log. Methods Comput. Sci.
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2023 — conf
EVA: a Tool for the Compositional Verification of AUTOSAR Models.
TACAS (2)
Alessandro Cimatti, Luca Cristoforetti, Alberto Griggio, Stefano Tonetta, Sara Corfini, Marco Di Natale, Florian Barrau
2023 J jnl
Formal Analysis and Verification of Max-Plus Linear Systems.
CoRR
Muhammad Syifa'ul Mufid, Andrea Micheli, Alessandro Abate, Alessandro Cimatti
2023 C ed.
Formal Methods for Industrial Critical Systems - 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023, Proceedings
FMICS
Alessandro Cimatti, Laura Titolo
2023 J jnl
GR(1) is equivalent to R(1).
Inf. Process. Lett.
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2023 — conf
SMT-Based Stability Verification of an Industrial Switched PI Control Systems.
DSN-W
Stylianos Basagiannis, Ludovico Battista, Anna Becchi, Alessandro Cimatti, Georgios Giantamidis, Sergio Mover, Alberto Tacchella, Stefano Tonetta, Vassilios A. Tsachouridis
2023 — conf
Searching for i-Good Lemmas to Accelerate Safety Model Checking.
CAV (2)
Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, Geguang Pu
2023 — conf
Set-Based Invariants over Polynomial Systems.
CILC
Alberto Casagrande, Alessandro Cimatti, Luca Dorigo, Carla Piazza, Stefano Tonetta
2023 B conf
Symbolic Model Checking of Relative Safety LTL Properties.
iFM
Alberto Bombardelli, Alessandro Cimatti, Stefano Tonetta, Marco Zamboni
2023 — conf
Towards Automatic Digitalization of Railway Engineering Schematics.
AI*IA
Stéfano Frizzo Stefenon, Marco Cristoforetti, Alessandro Cimatti
2023 — conf
Two formal methodologies of Model-Based Safety Assessment for Fault Tree Analysis.
ICSRS
Isabella Lanzani, Riccardo Scattolini, Enrico Zio, Alessandro Cimatti, Marco Bozzano, Stefano Tonetta
2022 — conf
A Formal IDE for Railways: Research Challenges.
SEFM Workshops
Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Angelo Susi
2022 A conf
A comprehensive framework for the analysis of automotive systems.
MoDELS
Alessandro Cimatti, Sara Corfini, Luca Cristoforetti, Marco Di Natale, Alberto Griggio, Stefano Puri, Stefano Tonetta
2022 B conf
A first-order logic characterisation of safety and co-safety languages.
FoSSaCS
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2022 J jnl
A first-order logic characterization of safety and co-safety languages.
CoRR
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2022 — conf
Abstraction Modulo Stability for Reverse Engineering.
CAV (1)
Anna Becchi, Alessandro Cimatti
2022 B conf
Analysis of Cyclic Fault Propagation via ASP.
LPNMR
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonás, Greg Kimberly
2022 J jnl
Assumption-based Runtime Verification.
Formal Methods Syst. Des.
Alessandro Cimatti, Chun Tian, Stefano Tonetta
2022 — conf
COMPASTA: Extending TASTE with Formal Design and Verification Functionality.
IMBSA
Alberto Bombardelli, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Massimo Nazaria, Edoardo Nicolodi, Stefano Tonetta
2022 A* conf
Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping.
AAAI
Stefan Panjkovic, Andrea Micheli, Alessandro Cimatti
2022 J jnl
Diagnosability of fair transition systems.
Artif. Intell.
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta, Viktória Vozárová
2022 — conf
Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation.
TACAS (2)
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Martin Jonás
2022 — conf
Formal Design and Validation of an Automatic Train Operation Control System.
RSSRail
Arturo Amendola, Lorenzo Barruffo, Marco Bozzano, Alessandro Cimatti, Salvatore De Simone, Eugenio Fedeli, Artem Gabbasov, Domenico Ernesto Garrubba, Massimiliano Girardi, Diana Serra, Roberto Tiella, Gianni Zampedri
2022 B conf
Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test.
ATVA
Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani
2022 J jnl
LTL falsification in infinite-state systems.
Inf. Comput.
Alessandro Cimatti, Alberto Griggio, Enrico Magnago
2022 — conf
NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems.
TACAS (1)
Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Andrea Ferrando, Lorenzo Pilati, Giuseppe Scaglione, Alberto Tacchella, Marco Zamboni
2022 — conf
Searching for Ribbon-Shaped Paths in Fair Transition Systems.
TACAS (1)
Marco Bozzano, Alessandro Cimatti, Stefano Tonetta, Viktória Vozárová
2022 J jnl
Semi-ProtoPNet Deep Neural Network for the Classification of Defective Power Grid Distribution Structures.
Sensors
Stéfano Frizzo Stefenon, Gurmail Singh, Kin Choong Yow, Alessandro Cimatti
2022 — conf
Symbolic Encoding of Reliability for the Design of Redundant Architectures.
ICPS
Antonio Tierno, Giuliano Turri, Alessandro Cimatti, Roberto Passerone
2022 — conf
The VMT-LIB Language and Tools.
SMT
Alessandro Cimatti, Alberto Griggio, Stefano Tonetta
2022 J jnl
Verification modulo theories.
Formal Methods Syst. Des.
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Marco Roveri, Stefano Tonetta
2022 B conf
Verification of SMT Systems with Quantifiers.
ATVA
Alessandro Cimatti, Alberto Griggio, Gianluca Redondi
2021 J jnl
A Comprehensive Approach to On-board Autonomy Verification and Validation.
ACM Trans. Intell. Syst. Technol.
Marco Bozzano, Alessandro Cimatti, Marco Roveri
2021 B conf
Assumption-Based Runtime Verification of Infinite-State Systems.
RV
Alessandro Cimatti, Chun Tian, Stefano Tonetta
2021 — conf
Automatic Design Space Exploration of Redundant Architectures.
ApplePies
Antonio Tierno, Giuliano Turri, Alessandro Cimatti, Roberto Passerone
2021 B conf
Automatic Discovery of Fair Paths in Infinite-State Transition Systems.
ATVA
Alessandro Cimatti, Alberto Griggio, Enrico Magnago
2021 C conf
Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans.
TIME
Michael Cashmore, Alessandro Cimatti, Daniele Magazzeni, Andrea Micheli, Parisa Zehtabi
2021 — conf
Efficient SMT-Based Analysis of Failure Propagation.
CAV (2)
Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, Alberto Griggio, Martin Jonás, Greg Kimberly
2021 — conf
Expressiveness of Extended Bounded Response LTL.
GandALF
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2021 B conf
Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis.
SEFM
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2021 — conf
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems.
CAV (1)
Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Stefano Tonetta
2021 J jnl
Model-based Safety Assessment of a Triple Modular Generator with xSAP.
Formal Aspects Comput.
Marco Bozzano, Alessandro Cimatti, Marco Gario, David Jones, Cristian Mattarei
2021 — conf
Optimization Modulo Non-linear Arithmetic via Incremental Linearization.
FroCoS
Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonás, Marco Roveri, Roberto Sebastiani, Patrick Trentin
2021 B conf
Proving the Existence of Fair Paths in Infinite-State Systems.
VMCAI
Alessandro Cimatti, Alberto Griggio, Enrico Magnago
2021 — conf
Reverse engineering with P-stable Abstractions.
OVERLAY@GandALF
Anna Becchi, Alessandro Cimatti, Enea Zaffanella
2021 B conf
SMT-Based Model Checking of Max-Plus Linear Systems.
CONCUR
Muhammad Syifa'ul Mufid, Andrea Micheli, Alessandro Abate, Alessandro Cimatti
2021 J jnl
The VMT-LIB Language and Tools.
CoRR
Alessandro Cimatti, Alberto Griggio, Stefano Tonetta
2021 A conf
Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning.
CADE
Alessandro Cimatti, Alberto Griggio, Gianluca Redondi
2020 — conf
A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System.
ISoLA (3)
Arturo Amendola, Anna Becchi, Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Giuseppe Scaglione, Angelo Susi, Alberto Tacchella, Matteo Tessi
2020 — conf
Computation of the Transient in Max-Plus Linear Systems via SMT-Solving.
FORMATS
Alessandro Abate, Alessandro Cimatti, Andrea Micheli, Muhammad Syifa'ul Mufid
2020 J jnl
Computation of the Transient in Max-Plus Linear Systems via SMT-Solving.
CoRR
Alessandro Abate, Alessandro Cimatti, Andrea Micheli, Muhammad Syifa'ul Mufid
2020 B conf
Reactive Synthesis from Extended Bounded Response LTL Specifications.
FMCAD
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2020 J jnl
Reactive Synthesis from Extended Bounded Response LTL Specifications.
CoRR
Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta
2020 J jnl
SMT-based satisfiability of first-order LTL with event freezing functions and metric operators.
Inf. Comput.
Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, Stefano Tonetta
2020 — conf
Safe Decomposition of Startup Requirements: Verification and Synthesis.
TACAS (1)
Alessandro Cimatti, Luca Geatti, Alberto Griggio, Greg Kimberly, Stefano Tonetta
2020 B conf
Synthesis of P-Stable Abstractions.
SEFM
Anna Becchi, Alessandro Cimatti, Enea Zaffanella
2020 A* conf
Temporal Planning with Intermediate Conditions and Effects.
AAAI
Alessandro Valentini, Andrea Micheli, Alessandro Cimatti
2019 — conf
ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics.
ARCH@CPSIoTWeek
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, Enea Zaffanella
2019 B conf
Assumption-Based Runtime Verification with Partial Observability and Resets.
RV
Alessandro Cimatti, Chun Tian, Stefano Tonetta
2019 — conf
COMPASS 3.0.
TACAS (1)
Marco Bozzano, Harold Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta
2019 — conf
Extending nuXmv with Timed Transition Systems and Timed Temporal Properties.
CAV (1)
Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, Stefano Tonetta
2019 J jnl
Formal reliability analysis of redundancy architectures.
Formal Aspects Comput.
Marco Bozzano, Alessandro Cimatti, Cristian Mattarei
2019 — conf
Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization.
SC-square@SIAM AG
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
2019 B conf
Model-Based Run-Time Synthesis of Architectural Configurations for Adaptive MILS Systems.
SAFECOMP
Alessandro Cimatti, Rance DeLong, Ivan Stojic, Stefano Tonetta
2019 B conf
NuRV: A nuXmv Extension for Runtime Verification.
RV
Alessandro Cimatti, Chun Tian, Stefano Tonetta
2019 A* conf
Robustness Envelopes for Temporal Plans.
AAAI
Michael Cashmore, Alessandro Cimatti, Daniele Magazzeni, Andrea Micheli, Parisa Zehtabi
2019 J jnl
Temporal Planning with Intermediate Conditions and Effects.
CoRR
Alessandro Valentini, Andrea Micheli, Alessandro Cimatti
2019 J jnl
Towards Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans.
CoRR
Michael Cashmore, Alessandro Cimatti, Daniele Magazzeni, Andrea Micheli, Parisa Zehtabi
2018 B conf
Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks.
FMCAD
Roberto Cavada, Alessandro Cimatti, Sergio Mover, Mirko Sessa, Giuseppe Cadavero, Giuseppe Scaglione
2018 A conf
Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization.
SAT
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018 B conf
Formal Specification and Verification of Dynamic Parametrized Architectures.
FM
Alessandro Cimatti, Ivan Stojic, Stefano Tonetta
2018 J jnl
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions.
ACM Trans. Comput. Log.
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018 Misc conf
Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions.
SYNASC
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018 J jnl
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF.
CoRR
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018 J jnl
Satisfiability Modulo Transcendental Functions via Incremental Linearization.
CoRR
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2018 J jnl
Strong temporal planning with uncontrollable durations.
Artif. Intell.
Alessandro Cimatti, Minh Do, Andrea Micheli, Marco Roveri, David E. Smith
2018 — conf
Symbolic execution with existential second-order constraints.
ESEC/SIGSOFT FSE
Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, Abhik Roychoudhury
2018 J jnl
Tightening the contract refinements of a system architecture.
Formal Methods Syst. Des.
Alessandro Cimatti, Ramiro Demasi, Stefano Tonetta
2018 — conf
Towards adaptive MILS System: Model- Based Design, Verification and Run-Time Adaptation: Slides.
MILS@DSN
Alessandro Cimatti, Rance DeLong, Ivan Stojic, Stefano Tonetta
2017 C ed.
28th International Workshop on Principles of Diagnosis (DX'17), Brescia, Italy, September 26-29, 2017
DX
Marina Zanella, Ingo Pill, Alessandro Cimatti
2017 — conf
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF.
TACAS (1)
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2017 — conf
SC-square: when Satisfiability Checking and Symbolic Computation join forces.
ARCADE@CADE
Erika Ábrahám, 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 B conf
SMT-based analysis of switching multi-domain linear Kirchhoff networks.
FMCAD
Alessandro Cimatti, Sergio Mover, Mirko Sessa
2017 A conf
Satisfiability Modulo Transcendental Functions via Incremental Linearization.
CADE
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
2017 B ed.
Software Engineering and Formal Methods - 15th International Conference, SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings
SEFM
Alessandro Cimatti, Marjan Sirjani
2017 — conf
Timed Failure Propagation Analysis for Spacecraft Engineering: The ESA Solar Orbiter Case Study.
IMBSA
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti
2017 A* conf
Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic.
AAAI
Alessandro Cimatti, Andrea Micheli, Marco Roveri
2016 A conf
A Lazy Approach to Temporal Epistemic Logic Model Checking.
AAMAS
Alessandro Cimatti, Marco Gario, Stefano Tonetta
2016 A* conf
Automated Synthesis of Timed Failure Propagation Graphs.
IJCAI
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti
2016 A* conf
Automated Verification and Tightening of Failure Propagation Models.
AAAI
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Gianni Zampedri
2016 A* conf
Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies.
AAAI
Alessandro Cimatti, Andrea Micheli, Marco Roveri
2016 J jnl
Dynamic controllability via Timed Game Automata.
Acta Informatica
Alessandro Cimatti, Luke Hunsberger, Andrea Micheli, Roberto Posenato, Marco Roveri
2016 B conf
From Electrical Switched Networks to Hybrid Automata.
FM
Alessandro Cimatti, Sergio Mover, Mirko Sessa
2016 — conf
Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations.
CAV (1)
Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, Sergio Mover
2016 J jnl
Infinite-state invariant checking with IC3 and predicate abstraction.
Formal Methods Syst. Des.
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
2016 — conf
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration.
CAV (2)
Marco Gario, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta, Kristin Yvonne Rozier
2016 B conf
Model-Based Design of an Energy-System Embedded Controller Using Taste.
FM
Roberto Cavada, Alessandro Cimatti, Luigi Crema, Mattia Roccabruna, Stefano Tonetta
2016 C conf
SC
CICM
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016 J jnl
Satisfiability Checking and Symbolic Computation.
CoRR
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016 J jnl
Satisfiability Checking meets Symbolic Computation (Project Paper).
CoRR
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016 J jnl
Satisfiability checking and symbolic computation.
ACM Commun. Comput. Algebra
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
2016 A conf
The xSAP Safety Analysis Platform.
TACAS
Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli, Gianni Zampedri
2016 B conf
Tightening a Contract Refinement.
SEFM
Alessandro Cimatti, Ramiro Demasi, Stefano Tonetta
2016 A conf
Verilog2SMV: A tool for word-level verification.
DATE
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
2015 J jnl
An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty.
Artif. Intell.
Alessandro Cimatti, Andrea Micheli, Marco Roveri
2015 — conf
Combining MILS with Contract-Based Design for Safety and Security Requirements.
SAFECOMP Workshops
Alessandro Cimatti, Rance DeLong, Davide Marcantonio, Stefano Tonetta
2015 B conf
Comparing Different Functional Allocations in Automated Air Traffic Control Design.
FMCAD
Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta, Kristin Y. Rozier
2015 J jnl
Contracts-refinement proof system for component-based embedded systems.
Sci. Comput. Program.
Alessandro Cimatti, Stefano Tonetta
2015 — conf
Efficient Anytime Techniques for Model-Based Safety Analysis.
CAV (1)
Marco Bozzano, Alessandro Cimatti, Alberto Griggio, Cristian Mattarei
2015 — conf
Formal Design and Safety Analysis of AIR6110 Wheel Brake System.
CAV (1)
Marco Bozzano, Alessandro Cimatti, Anthony Fernandes Pires, David Jones, Greg Kimberly, T. Petri, R. Robinson, Stefano Tonetta
2015 J jnl
Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic.
Log. Methods Comput. Sci.
Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta
2015 B conf
Formal Verification of Infinite-State BIP Models.
ATVA
Simon Bliudze, Alessandro Cimatti, Mohamad Jaber, Sergio Mover, Marco Roveri, Wajeb Saab, Qiang Wang
2015 J jnl
HRELTL: A temporal logic for hybrid systems.
Inf. Comput.
Alessandro Cimatti, Marco Roveri, Stefano Tonetta
2015 A conf
HyComp: An SMT-Based Model Checker for Hybrid Systems.
TACAS
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
2015 — conf
Parameter Synthesis with IC3 (Informal Presentation).
SynCoP
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
2015 A* conf
SMT-Based Validation of Timed Failure Propagation Graphs.
AAAI
Marco Bozzano, Alessandro Cimatti, Marco Gario, Andrea Micheli
2015 J jnl
Safety assessment of AltaRica models via symbolic model checking.
Sci. Comput. Program.
Marco Bozzano, Alessandro Cimatti, Oleg Lisagor, Cristian Mattarei, Sergio Mover, Marco Roveri, Stefano Tonetta
2015 J jnl
Solving strong controllability of temporal problems with uncertainty using SMT.
Constraints An Int. J.
Alessandro Cimatti, Andrea Micheli, Marco Roveri
2015 A* conf
Strong Temporal Planning with Uncontrollable Durations: A State-Space Approach.
AAAI
Alessandro Cimatti, Andrea Micheli, Marco Roveri
2015 J jnl
The xSAP Safety Analysis Platform.
CoRR
Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli, Gianni Zampedri
2014 — conf
An Integrated Process for FDIR Design in Aerospace.
IMBSA
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Régis De Ferluc, Marco Gario, Andrea Guiotto, Yuri Yushtein
2014 J jnl
Automated Planning and Model Checking (Dagstuhl Seminar 14482).
Dagstuhl Reports
Alessandro Cimatti, Stefan Edelkamp, Maria Fox, Daniele Magazzeni, Erion Plaku
2014 J jnl
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories.
CoRR
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2014 A conf
Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic.
TACAS
Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta
2014 B conf
Formal Safety Assessment via Contract-Based Design.
ATVA
Marco Bozzano, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta
2014 A conf
IC3 Modulo Theories via Implicit Predicate Abstraction.
TACAS
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
2014 J jnl
Quantifier-free encoding of invariants for hybrid systems.
Formal Methods Syst. Des.
Alessandro Cimatti, Sergio Mover, Stefano Tonetta
2014 C conf
Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation.
TIME
Alessandro Cimatti, Luke Hunsberger, Andrea Micheli, Roberto Posenato, Marco Roveri
2014 J jnl
Spacecraft early design validation using formal methods.
Reliab. Eng. Syst. Saf.
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Panagiotis Katsaros, Konstantinos Mokos, Viet Yen Nguyen, Thomas Noll, Bart Postma, Marco Roveri
2014 A* conf
The nuXmv Symbolic Model Checker.
CAV
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, Stefano Tonetta
2014 B conf
Towards Pareto-optimal parameter synthesis for monotonic cost functions.
FMCAD
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario, Alberto Griggio
2014 A* conf
Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty.
AAAI
Alessandro Cimatti, Luke Hunsberger, Andrea Micheli, Marco Roveri
2014 A* conf
Verifying LTL Properties of Hybrid Systems with K-Liveness.
CAV
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
2013 — conf
A Formal Framework for the Specification, Verification and Synthesis of Diagnosers.
AAAI (Late-Breaking Developments)
Marco Bozzano, Alessandro Cimatti, Marco Gario, Stefano Tonetta
2013 A conf
A Modular Approach to MaxSAT Modulo Theories.
SAT
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
2013 B conf
Automated Analysis of Reliability Architectures.
ICECCS
Marco Bozzano, Alessandro Cimatti, Cristian Mattarei
2013 — conf
Efficient Analysis of Reliability Architectures via Predicate Abstraction.
Haifa Verification Conference
Marco Bozzano, Alessandro Cimatti, Cristian Mattarei
2013 J jnl
IC3 Modulo Theories via Implicit Predicate Abstraction.
CoRR
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
2013 A* conf
OCRA: A tool for checking the refinement of temporal contracts.
ASE
Alessandro Cimatti, Michele Dorigatti, Stefano Tonetta
2013 B conf
Parameter synthesis with IC3.
FMCAD
Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta
2013 B conf
SMT-Based Software Model Checking - Explicit Scheduler, Symbolic Threads.
ATVA
Alessandro Cimatti
2013 J jnl
SMT-based scenario verification for hybrid systems.
Formal Methods Syst. Des.
Alessandro Cimatti, Sergio Mover, Stefano Tonetta
2013 J jnl
Software Model Checking SystemC.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Alessandro Cimatti, Iman Narasamdya, Marco Roveri
2013 A conf
The MathSAT5 SMT Solver.
TACAS
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani
2013 Misc conf
Time-aware relational abstractions for hybrid systems.
EMSOFT
Sergio Mover, Alessandro Cimatti, Ashish Tiwari, Stefano Tonetta
2013 A* conf
Timelines with Temporal Uncertainty.
AAAI
Alessandro Cimatti, Andrea Micheli, Marco Roveri
2012 — conf
A Property-Based Proof System for Contract-Based Design.
EUROMICRO-SEAA
Alessandro Cimatti, Stefano Tonetta
2012 B conf
A quantifier-free SMT encoding of non-linear hybrid automata.
FMCAD
Alessandro Cimatti, Sergio Mover, Stefano Tonetta
2012 B conf
Application of SMT solvers to hybrid system verification.
FMCAD
Alessandro Cimatti
2012 A* conf
Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System.
CAV
Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, Tiziana Rizzo, Marco Roveri, Angela Sanseviero, Andrei Tchaltsev
2012 A* conf
SMT-Based Verification of Hybrid Systems.
AAAI
Alessandro Cimatti, Sergio Mover, Stefano Tonetta
2012 A* conf
Software Model Checking via IC3.
CAV
Alessandro Cimatti, Alberto Griggio
2012 J jnl
Software Model Checking with Explicit Scheduler and Symbolic Threads
Log. Methods Comput. Sci.
Alessandro Cimatti, Iman Narasamdya, Marco Roveri
2012 A conf
Solving Temporal Problems Using SMT: Strong Controllability.
CP
Alessandro Cimatti, Andrea Micheli, Marco Roveri
2012 A* conf
Solving Temporal Problems Using SMT: Weak Controllability.
AAAI
Alessandro Cimatti, Andrea Micheli, Marco Roveri
2012 A* conf
Symbolic Synthesis of Observability Requirements for Diagnosability.
AAAI
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Xavier Olive
2012 A ed.
Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings
SAT
Alessandro Cimatti, Roberto Sebastiani
2012 J jnl
Validation of requirements for hybrid systems: A formal approach.
ACM Trans. Softw. Eng. Methodol.
Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta
2012 B conf
Verification of parametric system designs.
FMCAD
Alessandro Cimatti, Iman Narasamdya, Marco Roveri
2011 A* conf
A Comprehensive Approach to On-Board Autonomy Verification and Validation.
IJCAI
Marco Bozzano, Alessandro Cimatti, Marco Roveri, Andrei Tchaltsev
2011 — conf
An Analytic Evaluation of SystemC Encodings in Promela.
SPIN
Daniele Campana, Alessandro Cimatti, Iman Narasamdya, Marco Roveri
2011 A conf
Boosting Lazy Abstraction for SystemC with Partial Order Reduction.
TACAS
Alessandro Cimatti, Iman Narasamdya, Marco Roveri
2011 J jnl
Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories.
J. Artif. Intell. Res.
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2011 J jnl
Conformant Planning via Symbolic Model Checking
CoRR
Alessandro Cimatti, Marco Roveri
2011 A* conf
Efficient Scenario Verification for Hybrid Automata.
CAV
Alessandro Cimatti, Sergio Mover, Stefano Tonetta
2011 J jnl
Formalizing requirements with object models and temporal constraints.
Softw. Syst. Model.
Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta
2011 — conf
HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction.
EUROMICRO-SEAA
Alessandro Cimatti, Sergio Mover, Stefano Tonetta
2011 A* conf
Kratos - A Software Model Checker for SystemC.
CAV
Alessandro Cimatti, Alberto Griggio, Andrea Micheli, Iman Narasamdya, Marco Roveri
2011 — conf
OthelloPlay: a plug-in based tool for requirement formalization and validation.
TOPI@ICSE
Roberto Cavada, Alessandro Cimatti, Andrea Micheli, Marco Roveri, Angelo Susi, Stefano Tonetta
2011 B conf
Proving and explaining the unfeasibility of message sequence charts for hybrid systems.
FMCAD
Alessandro Cimatti, Sergio Mover, Stefano Tonetta
2011 J jnl
Safety, Dependability and Performance Analysis of Extended AADL Models.
Comput. J.
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri
2011 J jnl
Symbolic Model Checking and Safety Assessment of Altarica models.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Marco Bozzano, Alessandro Cimatti, Oleg Lisagor, Cristian Mattarei, Sergio Mover, Marco Roveri, Stefano Tonetta
2010 A* conf
A Model Checker for AADL.
CAV
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer
2010 B conf
Applying SMT in symbolic execution of microcode.
FMCAD
Anders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev
2010 J jnl
Efficient generation of craig interpolants in satisfiability modulo theories.
ACM Trans. Comput. Log.
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2010 — conf
Formalization and validation of a subset of the European Train Control System.
ICSE (2)
Angelo Chiappini, Alessandro Cimatti, Luca Macchi, Oscar Rebollo, Marco Roveri, Angelo Susi, Stefano Tonetta, Berardino Vittorini
2010 C conf
From Sequential Extended Regular Expressions to NFA with Symbolic Labels.
CIAA
Alessandro Cimatti, Sergio Mover, Marco Roveri, Stefano Tonetta
2010 — conf
Model Checking of Hybrid Systems Using Shallow Synchronization.
FMOODS/FORTE
Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta
2010 C conf
Parametric analysis of distributed firm real-time systems: A case study.
ETFA
Thi Thieu Hoa Le, Luigi Palopoli, Roberto Passerone, Yusi Ramadian, Alessandro Cimatti
2010 A* conf
RATSY - A New Requirements Analysis Tool with Synthesis.
CAV
Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan, Richard Seeber
2010 — conf
SMT-Based Software Model Checking.
SPIN
Alessandro Cimatti
2010 A conf
Satisfiability Modulo the Theory of Costs: Foundations and Applications.
TACAS
Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani, Cristian Stenico
2010 A conf
Tighter integration of BDDs and SMT for Predicate Abstraction.
DATE
Alessandro Cimatti, Anders Franzén, Alberto Griggio, Krishnamani Kalyanasundaram, Marco Roveri
2010 B conf
Verifying SystemC: A software model checking approach.
FMCAD
Alessandro Cimatti, Andrea Micheli, Iman Narasamdya, Marco Roveri
2009 C conf
Codesign of dependable systems: A component-based modeling language.
MEMOCODE
Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll
2009 J jnl
Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis.
Ann. Math. Artif. Intell.
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
2009 J jnl
Efficient Generation of Craig Interpolants in Satisfiability Modulo Theories
CoRR
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2009 — conf
Formalization and Validation of Safety-Critical Requirements
FMA
Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta
2009 A conf
Interpolant Generation for UTVPI.
CADE
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2009 — conf
Model-Based Codesign of Critical Embedded Systems.
ACES-MB@MoDELS
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri
2009 A* conf
Requirements Validation for Hybrid Systems.
CAV
Alessandro Cimatti, Marco Roveri, Stefano Tonetta
2009 J jnl
Software Model Checking via Large-Block Encoding
CoRR
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
2009 B conf
Software model checking via large-block encoding.
FMCAD
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
2009 B conf
Structure-aware computation of predicate abstraction.
FMCAD
Alessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri
2009 A* conf
Supporting Requirements Validation: The EuRailCheck Tool.
ASE
Roberto Cavada, Alessandro Cimatti, Alessandro Mariotti, Cristian Mattarei, Andrea Micheli, Sergio Mover, Marco Pensallorto, Marco Roveri, Angelo Susi, Stefano Tonetta
2009 B conf
The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems.
SAFECOMP
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri
2009 — conf
Verification and performance evaluation of aadl models.
ESEC/SIGSOFT FSE
Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll
2008 — ch.
Automated Planning.
Handbook of Knowledge Representation
Alessandro Cimatti, Marco Pistore, Paolo Traverso
2008 B conf
Diagnostic Information for Realizability.
VMCAI
Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Andrei Tchaltsev
2008 A conf
Efficient Interpolant Generation in Satisfiability Modulo Theories.
TACAS
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2008 B ed.
Formal Methods in Computer-Aided Design, FMCAD 2008, Portland, Oregon, USA, 17-20 November 2008
FMCAD
Alessandro Cimatti, Robert B. Jones
2008 C conf
From Informal Requirements to Property-Driven Formal Validation.
FMICS
Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta
2008 B conf
Object Models with Temporal Constraints.
SEFM
Alessandro Cimatti, Marco Roveri, Angelo Susi, Stefano Tonetta
2008 J jnl
Symbolic Compilation of PSL.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Alessandro Cimatti, Marco Roveri, Stefano Tonetta
2008 A conf
Symbolic Computation of Schedulability Regions Using Parametric Timed Automata.
RTSS
Alessandro Cimatti, Luigi Palopoli, Yusi Ramadian
2008 A* conf
The MathSAT 4SMT Solver.
CAV
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
2007 A* conf
A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems.
CAV
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani
2007 A conf
A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories.
SAT
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
2007 A* conf
Boolean Abstraction for Temporal Logic Satisfiability.
CAV
Alessandro Cimatti, Marco Roveri, Viktor Schuppan, Stefano Tonetta
2007 B conf
Computing Predicate Abstractions by Integrating BDDs and SMT Solvers.
FMCAD
Roberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar
2007 B conf
Symbolic Fault Tree Analysis for Reactive Systems.
ATVA
Marco Bozzano, Alessandro Cimatti, Francesco Tapparo
2007 J jnl
Symbolic Implementation of Alternating Automata.
Int. J. Found. Comput. Sci.
Roderick Bloem, Alessandro Cimatti, Ingo Pill, Marco Roveri
2007 A conf
Syntactic Optimizations for PSL Verification.
TACAS
Alessandro Cimatti, Marco Roveri, Stefano Tonetta
2007 B conf
Verifying Heap-Manipulating Programs in an SMT Framework.
ATVA
Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti
2006 — conf
A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis.
MoChArt
Piergiorgio Bertoli, Marco Bozzano, Alessandro Cimatti
2006 — conf
Building Efficient Decision Procedures on Top of SAT Solvers.
SFM
Alessandro Cimatti, Roberto Sebastiani
2006 B conf
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis.
LPAR
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani
2006 J jnl
Efficient theory combination via boolean search.
Inf. Comput.
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani
2006 — ed.
Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures
SFM
Marco Bernardo, Alessandro Cimatti
2006 A* conf
Formal analysis of hardware requirements.
DAC
Ingo Pill, Simone Semprini, Roberto Cavada, Marco Roveri, Roderick Bloem, Alessandro Cimatti
2006 B conf
From PSL to NBA: a Modular Symbolic Encoding.
FMCAD
Alessandro Cimatti, Marco Roveri, Simone Semprini, Stefano Tonetta
2006 — ed.
Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, PDPAR@CAV 2005, Edinburgh, UK, July 12, 2005
PDPAR@CAV
Alessandro Armando, Alessandro Cimatti
2006 A conf
Stong Cyclic Planning Under Partial Observability.
ECAI
Piergiorgio Bertoli, Alessandro Cimatti, Marco Pistore
2006 J jnl
Strong planning under partial observability.
Artif. Intell.
Piergiorgio Bertoli, Alessandro Cimatti, Marco Roveri, Paolo Traverso
2006 C conf
Symbolic Implementation of Alternating Automata.
CIAA
Roderick Bloem, Alessandro Cimatti, Ingo Pill, Marco Roveri, Simone Semprini
2006 B conf
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in
LPAR
Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani
2006 A* conf
Towards Strong Cyclic Planning under Partial Observability.
ICAPS
Piergiorgio Bertoli, Alessandro Cimatti, Marco Pistore
2005 A conf
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic.
TACAS
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2005 A* conf
Efficient Satisfiability Modulo Theories via Delayed Theory Combination.
CAV
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani
2005 — conf
Encoding RTL Constructs for MathSAT: a Preliminary Report.
PDPAR@CAV
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Ziyad Hanna, Zurab Khasidashvili, Amit Palti, Roberto Sebastiani
2005 J jnl
MathSAT: Tight Integration of SAT and Mathematical Decision Procedures.
J. Autom. Reason.
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2005 — conf
Preface.
PDPAR@CAV
Alessandro Armando, Alessandro Cimatti
2005 A conf
The MathSAT 3 System.
CADE
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2004 B conf
Bounded Verification of Past LTL.
FMCAD
Alessandro Cimatti, Marco Roveri, Daniel Sheridan
2004 J jnl
Conformant planning via symbolic model checking and heuristic search.
Artif. Intell.
Alessandro Cimatti, Marco Roveri, Piergiorgio Bertoli
2004 A conf
Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains.
ECAI
Piergiorgio Bertoli, Alessandro Cimatti, Paolo Traverso
2004 A conf
Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems.
ECAI
Floris Roelofsen, Luciano Serafini, Alessandro Cimatti
2004 — conf
Verifying Industrial Hybrid Systems with MathSAT.
BMC@CAV
Gilles Audemard, Marco Bozzano, Alessandro Cimatti, Roberto Sebastiani
2003 A* conf
A Framework for Planning with Extended Goals under Partial Observability.
ICAPS
Piergiorgio Bertoli, Alessandro Cimatti, Marco Pistore, Paolo Traverso
2003 A conf
Bounded Model Checking for Past LTL.
TACAS
Marco Benedetti, Alessandro Cimatti
2003 J jnl
Bounded model checking.
Adv. Comput.
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu
2003 A* conf
Formal Verification of Diagnosability via Symbolic Model Checking.
IJCAI
Alessandro Cimatti, Charles Pecheur, Roberto Cavada
2003 J jnl
Weak, strong, and strong cyclic planning via symbolic model checking.
Artif. Intell.
Alessandro Cimatti, Marco Pistore, Marco Roveri, Paolo Traverso
2002 A conf
A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions.
CADE
Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani
2002 C conf
Bounded Model Checking for Timed Systems.
FORTE
Gilles Audemard, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani
2002 — conf
Improving Heuristics for Planning as Search in Belief Space.
AIPS
Piergiorgio Bertoli, Alessandro Cimatti
2002 B conf
Improving the Encoding of LTL Model Checking into SAT.
VMCAI
Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani
2002 — conf
Integrating BDD-Based and SAT-Based Symbolic Model Checking.
FroCoS
Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella
2002 Misc conf
Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements.
AISC
Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani
2002 A* conf
NuSMV 2: An OpenSource Tool for Symbolic Model Checking.
CAV
Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella
2002 A conf
Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking.
ECAI
Piergiorgio Bertoli, Alessandro Cimatti, John K. Slaney, Sylvie Thiébaux
2002 — conf
Validation of Multiagent Systems by Symbolic Model Checking.
AOSE
Massimo Benerecetti, Alessandro Cimatti
2001 A* conf
Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning.
IJCAI
Piergiorgio Bertoli, Alessandro Cimatti, Marco Roveri
2001 A* conf
Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking.
IJCAI
Piergiorgio Bertoli, Alessandro Cimatti, Marco Roveri, Paolo Traverso
2001 A conf
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking.
TACAS
Alessandro Cimatti, Marco Roveri, Piergiorgio Bertoli
2000 J jnl
Conformant Planning via Symbolic Model Checking.
J. Artif. Intell. Res.
Alessandro Cimatti, Marco Roveri
2000 — conf
Industrial Applications of Model Checking.
MOVEP
Alessandro Cimatti
2000 J jnl
NUSMV: A New Symbolic Model Checker.
Int. J. Softw. Tools Technol. Transf.
Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri
2000 J jnl
Verification of a safety-critical railway interlocking system with real-time constraints.
Sci. Comput. Program.
Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia
1999 — conf
Conformant Planning via Model Checking.
ECP
Alessandro Cimatti, Marco Roveri
1999 — ed.
First International Workshop on Symbolic Model Checking, SMC 1999, associated to FLoC'99, the 1999 Federated Logic Conference, Trento, Italy, July 6, 1999
SMC@FLoC
Alessandro Cimatti, Orna Grumberg
1999 B conf
Formal Specification and Development of a Safety-Critical Train Management System.
SAFECOMP
Angelo Chiappini, Alessandro Cimatti, Carmen Porzia, G. Rotondo, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita
1999 — conf
Formal Specification and Validation of a Vital Communication Protocol.
World Congress on Formal Methods
Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita
1999 A* conf
NUSMV: A New Symbolic Model Verifier.
CAV
Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri
1999 — conf
Preface.
SMC@FLoC
Alessandro Cimatti, Orna Grumberg
1999 A* conf
Symbolic Model Checking Using SAT Procedures instead of BDDs.
DAC
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu
1999 A conf
Symbolic Model Checking without BDDs.
TACAS
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu
1998 J jnl
A Many-Sorted Natural Deduction.
Comput. Intell.
Alessandro Cimatti, Fausto Giunchiglia, Richard W. Weyhrauch
1998 B conf
A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools.
SAFECOMP
Piergiorgio Bertoli, Alessandro Cimatti, Fausto Giunchiglia, Paolo Traverso
1998 — conf
Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic Domains.
AAAI/IAAI
Alessandro Cimatti, Marco Roveri, Paolo Traverso
1998 J jnl
Formal Verification of a Railway Interlocking System using Model Checking.
Formal Aspects Comput.
Alessandro Cimatti, Fausto Giunchiglia, Giorgio Mongardi, Dario Romano, Fernando Torielli, Paolo Traverso
1998 B conf
Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System.
SAFECOMP
Alessandro Cimatti, Fausto Giunchiglia, Giorgio Mongardi, Dario Romano, Fernando Torielli, Paolo Traverso
1998 — conf
Strong Planning in Non-Deterministic Domains Via Model Checking.
AIPS
Alessandro Cimatti, Marco Roveri, Paolo Traverso
1998 — conf
Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints.
FTCS
Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia
1997 A* conf
A Provably Correct Embedded Verifier for the Certification of Safety Critical Software.
CAV
Alessandro Cimatti, Fausto Giunchiglia, Paolo Pecchiari, Bruno Pietra, Joe Profeta, Dario Romano, Paolo Traverso, Bing Yu
1997 — conf
Planning via Model Checking: A Decision Procedure for
ECP
Alessandro Cimatti, Fausto Giunchiglia, Enrico Giunchiglia, Paolo Traverso
1996 J jnl
Computational reflection via mechanized logical deduction.
Int. J. Intell. Syst.
Alessandro Cimatti, Paolo Traverso
1996 — conf
Formal Specification of Beliefs in Multi-Agent Systems.
ATAL
Massimo Benerecetti, Alessandro Cimatti, Enrico Giunchiglia, Fausto Giunchiglia, Luciano Serafini
1996 — conf
Mechanizing Multi-Agent Reasoning with Belief Contexts.
FAPR
Alessandro Cimatti, Luciano Serafini
1996 J jnl
Visual representation of natural language scene descriptions.
IEEE Trans. Syst. Man Cybern. Part B
Enrico Giunchiglia, Alessandro Armando, Paolo Traverso, Alessandro Cimatti
1995 — conf
Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance.
ICMAS
Alessandro Cimatti, Luciano Serafini
1994 C conf
Introspective Metatheoretic Reasoning.
META
Fausto Giunchiglia, Alessandro Cimatti
1994 J jnl
MRG: Building planers for real-world complex applications.
Appl. Artif. Intell.
Paolo Traverso, Alessandro Cimatti, Luca Spalazzi, Alessandro Armando, Enrico Giunchiglia
1994 — conf
Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study.
ECAI Workshop on Agent Theories, Architectures, and Languages
Alessandro Cimatti, Luciano Serafini
1993 — conf
Building and Executing Proof Strategies in a Formal Metatheory.
AI*IA
Alessandro Armando, Alessandro Cimatti, Luca Viganò
1992 A conf
Beyond the Single Planning Paradigm: Introspective Planning.
ECAI
Paolo Traverso, Alessandro Cimatti, Luca Spalazzi