Beyond the Single Planning Paradigm: Introspective Planning. - Paolo Traverso; Alessandro Cimatti; Luca Spalazzi (ECAI, 1992)

Building and Executing Proof Strategies in a Formal Metatheory. - Alessandro Armando; Alessandro Cimatti; Luca Viganò 001 (AI*IA, 1993)

Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study. - Alessandro Cimatti; Luciano Serafini (ECAI Workshop on Agent Theories, Architectures, and Languages, 1994)

Introspective Metatheoretic Reasoning. - Fausto Giunchiglia; Alessandro Cimatti (META, 1994)

MRG: Building planers for real-world complex applications. - Paolo Traverso; Alessandro Cimatti; Luca Spalazzi; Alessandro Armando; Enrico Giunchiglia (Appl. Artif. Intell., 1994)

Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance. - Alessandro Cimatti; Luciano Serafini (ICMAS, 1995)

Formal Specification of Beliefs in Multi-Agent Systems. - Massimo Benerecetti; Alessandro Cimatti; Enrico Giunchiglia; Fausto Giunchiglia; Luciano Serafini (ATAL, 1996)

Mechanizing Multi-Agent Reasoning with Belief Contexts. - Alessandro Cimatti; Luciano Serafini (FAPR, 1996)

Computational reflection via mechanized logical deduction. - Alessandro Cimatti; Paolo Traverso (Int. J. Intell. Syst., 1996)

Visual representation of natural language scene descriptions. - Enrico Giunchiglia; Alessandro Armando; Paolo Traverso; Alessandro Cimatti (IEEE Trans. Syst. Man Cybern. Part B, 1996)

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 (CAV, 1997)

Planning via Model Checking: A Decision Procedure for AR. - Alessandro Cimatti; Fausto Giunchiglia; Enrico Giunchiglia; Paolo Traverso (ECP, 1997)

Automatic OBDD-Based Generation of Universal Plans in Non-Deterministic Domains. - Alessandro Cimatti; Marco Roveri; Paolo Traverso (AAAI/IAAI, 1998)

Strong Planning in Non-Deterministic Domains Via Model Checking. - Alessandro Cimatti; Marco Roveri; Paolo Traverso (AIPS, 1998)

A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools. - Piergiorgio Bertoli; Alessandro Cimatti; Fausto Giunchiglia; Paolo Traverso (SAFECOMP, 1998)

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 (SAFECOMP, 1998)

A Many-Sorted Natural Deduction. - Alessandro Cimatti; Fausto Giunchiglia; Richard W. Weyhrauch (Comput. Intell., 1998)

Formal Verification of a Railway Interlocking System using Model Checking. - Alessandro Cimatti; Fausto Giunchiglia; Giorgio Mongardi; Dario Romano; Fernando Torielli; Paolo Traverso (Formal Aspects Comput., 1998)

NUSMV: A New Symbolic Model Verifier. - Alessandro Cimatti; Edmund M. Clarke; Fausto Giunchiglia; Marco Roveri (CAV, 1999)

Symbolic Model Checking Using SAT Procedures instead of BDDs. - Armin Biere; Alessandro Cimatti; Edmund M. Clarke; Masahiro Fujita; Yunshan Zhu (DAC, 1999)

Conformant Planning via Model Checking. - Alessandro Cimatti; Marco Roveri (ECP, 1999)

Formal Specification and Validation of a Vital Communication Protocol. - Alessandro Cimatti; P. L. Pieraccini; Roberto Sebastiani; Paolo Traverso; Adolfo Villafiorita (World Congress on Formal Methods, 1999)

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 (SAFECOMP, 1999)

Symbolic Model Checking without BDDs. - Armin Biere; Alessandro Cimatti; Edmund M. Clarke; Yunshan Zhu (TACAS, 1999)

Preface. - Alessandro Cimatti; Orna Grumberg (SMC@FLoC, 1999)

Industrial Applications of Model Checking. - Alessandro Cimatti (MOVEP, 2000)

Conformant Planning via Symbolic Model Checking. - Alessandro Cimatti; Marco Roveri (J. Artif. Intell. Res., 2000)

Verification of a safety-critical railway interlocking system with real-time constraints. - Vicky Hartonas-Garmhausen; Sérgio Vale Aguiar Campos; Alessandro Cimatti; Edmund M. Clarke; Fausto Giunchiglia (Sci. Comput. Program., 2000)

NUSMV: A New Symbolic Model Checker. - Alessandro Cimatti; Edmund M. Clarke; Fausto Giunchiglia; Marco Roveri (Int. J. Softw. Tools Technol. Transf., 2000)

Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning. - Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri (IJCAI, 2001)

Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking. - Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri; Paolo Traverso (IJCAI, 2001)

Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking. - Alessandro Cimatti; Marco Roveri; Piergiorgio Bertoli (TACAS, 2001)

Improving Heuristics for Planning as Search in Belief Space. - Piergiorgio Bertoli; Alessandro Cimatti (AIPS, 2002)

Integrating Boolean and Mathematical Solving: Foundations, Basic Algorithms, and Requirements. - Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani (AISC, 2002)

Validation of Multiagent Systems by Symbolic Model Checking. - Massimo Benerecetti; Alessandro Cimatti (AOSE, 2002)

A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. - Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani (CADE, 2002)

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 (CAV, 2002)

Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking. - Piergiorgio Bertoli; Alessandro Cimatti; John K. Slaney; Sylvie Thiébaux (ECAI, 2002)

Bounded Model Checking for Timed Systems. - Gilles Audemard; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani (FORTE, 2002)

Integrating BDD-Based and SAT-Based Symbolic Model Checking. - Alessandro Cimatti; Enrico Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; Armando Tacchella (FroCoS, 2002)

Improving the Encoding of LTL Model Checking into SAT. - Alessandro Cimatti; Marco Pistore; Marco Roveri; Roberto Sebastiani (VMCAI, 2002)

A Framework for Planning with Extended Goals under Partial Observability. - Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Paolo Traverso (ICAPS, 2003)

Formal Verification of Diagnosability via Symbolic Model Checking. - Alessandro Cimatti; Charles Pecheur; Roberto Cavada (IJCAI, 2003)

Bounded Model Checking for Past LTL. - Marco Benedetti; Alessandro Cimatti (TACAS, 2003)

Bounded model checking. - Armin Biere; Alessandro Cimatti; Edmund M. Clarke; Ofer Strichman; Yunshan Zhu (Adv. Comput., 2003)

Weak, strong, and strong cyclic planning via symbolic model checking. - Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso (Artif. Intell., 2003)

Interleaving Execution and Planning for Nondeterministic, Partially Observable Domains. - Piergiorgio Bertoli; Alessandro Cimatti; Paolo Traverso (ECAI, 2004)

Many Hands Make Light Work: Localized Satisfiability for Multi-Context Systems. - Floris Roelofsen; Luciano Serafini; Alessandro Cimatti (ECAI, 2004)

Bounded Verification of Past LTL. - Alessandro Cimatti; Marco Roveri; Daniel Sheridan (FMCAD, 2004)

Conformant planning via symbolic model checking and heuristic search. - Alessandro Cimatti; Marco Roveri; Piergiorgio Bertoli (Artif. Intell., 2004)

Verifying Industrial Hybrid Systems with MathSAT. - Gilles Audemard; Marco Bozzano; Alessandro Cimatti; Roberto Sebastiani (BMC@CAV, 2004)

The MathSAT 3 System. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Peter van Rossum; Stephan Schulz 001; Roberto Sebastiani (CADE, 2005)

Efficient Satisfiability Modulo Theories via Delayed Theory Combination. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani (CAV, 2005)

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 001; Roberto Sebastiani (TACAS, 2005)

Preface. - Alessandro Armando; Alessandro Cimatti (PDPAR@CAV, 2005)

Encoding RTL Constructs for MathSAT: a Preliminary Report. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Ziyad Hanna; Zurab Khasidashvili; Amit Palti; Roberto Sebastiani (PDPAR@CAV, 2005)

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Peter van Rossum; Stephan Schulz 001; Roberto Sebastiani (J. Autom. Reason., 2005)

Towards Strong Cyclic Planning under Partial Observability. - Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore (ICAPS, 2006)

Formal analysis of hardware requirements. - Ingo Pill; Simone Semprini; Roberto Cavada; Marco Roveri; Roderick Bloem; Alessandro Cimatti (DAC, 2006)

Stong Cyclic Planning Under Partial Observability. - Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore (ECAI, 2006)

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

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Alessandro Santuari; Roberto Sebastiani (LPAR, 2006)

A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis. - Piergiorgio Bertoli; Marco Bozzano; Alessandro Cimatti (MoChArt, 2006)

Building Efficient Decision Procedures on Top of SAT Solvers. - Alessandro Cimatti; Roberto Sebastiani (SFM, 2006)

Symbolic Implementation of Alternating Automata. - Roderick Bloem; Alessandro Cimatti; Ingo Pill; Marco Roveri; Simone Semprini (CIAA, 2006)

Strong planning under partial observability. - Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri; Paolo Traverso (Artif. Intell., 2006)

Efficient theory combination via boolean search. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Tommi A. Junttila; Silvio Ranise; Peter van Rossum; Roberto Sebastiani (Inf. Comput., 2006)

Symbolic Fault Tree Analysis for Reactive Systems. - Marco Bozzano; Alessandro Cimatti; Francesco Tapparo (ATVA, 2007)

Verifying Heap-Manipulating Programs in an SMT Framework. - Zvonimir Rakamaric; Roberto Bruttomesso; Alan J. Hu; Alessandro Cimatti (ATVA, 2007)

A Lazy and Layered SMT($ mathcal{BV}$) Solver for Hard Industrial Verification Problems. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Ziyad Hanna; Alexander Nadel; Amit Palti; Roberto Sebastiani (CAV, 2007)

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

Computing Predicate Abstractions by Integrating BDDs and SMT Solvers. - Roberto Cavada; Alessandro Cimatti; Anders Franzén; Krishnamani Kalyanasundaram; Marco Roveri; R. K. Shyamasundar (FMCAD, 2007)

A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (SAT, 2007)

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

Symbolic Implementation of Alternating Automata. - Roderick Bloem; Alessandro Cimatti; Ingo Pill; Marco Roveri (Int. J. Found. Comput. Sci., 2007)

The MathSAT 4SMT Solver. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani (CAV, 2008)

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

Symbolic Computation of Schedulability Regions Using Parametric Timed Automata. - Alessandro Cimatti; Luigi Palopoli 002; Yusi Ramadian (RTSS, 2008)

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

Efficient Interpolant Generation in Satisfiability Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (TACAS, 2008)

Diagnostic Information for Realizability. - Alessandro Cimatti; Marco Roveri; Viktor Schuppan; Andrei Tchaltsev (VMCAI, 2008)

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

Automated Planning. - Alessandro Cimatti; Marco Pistore; Paolo Traverso (Handbook of Knowledge Representation, 2008)

Interpolant Generation for UTVPI. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (CADE, 2009)

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

Software model checking via large-block encoding. - Dirk Beyer 001; Alessandro Cimatti; Alberto Griggio; M. Erkan Keremoglu; Roberto Sebastiani (FMCAD, 2009)

Structure-aware computation of predicate abstraction. - Alessandro Cimatti; Jori Dubrovin; Tommi A. Junttila; Marco Roveri (FMCAD, 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)

Codesign of dependable systems: A component-based modeling language. - Marco Bozzano; Alessandro Cimatti; Marco Roveri; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll 001 (MEMOCODE, 2009)

Model-Based Codesign of Critical Embedded Systems. - Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll 001; Marco Roveri (ACES-MB@MoDELS, 2009)

The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. - Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll 001; Marco Roveri (SAFECOMP, 2009)

Verification and performance evaluation of aadl models. - Marco Bozzano; Alessandro Cimatti; Marco Roveri; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll 001 (ESEC/SIGSOFT FSE, 2009)

Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani (Ann. Math. Artif. Intell., 2009)

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

RATSY - A New Requirements Analysis Tool with Synthesis. - Roderick Bloem; Alessandro Cimatti; Karin Greimel; Georg Hofferek; Robert Könighofer; Marco Roveri; Viktor Schuppan; Richard Seeber (CAV, 2010)

A Model Checker for AADL. - Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll 001; Marco Roveri; Ralf Wimmer 001 (CAV, 2010)

Tighter integration of BDDs and SMT for Predicate Abstraction. - Alessandro Cimatti; Anders Franzén; Alberto Griggio; Krishnamani Kalyanasundaram; Marco Roveri (DATE, 2010)

Parametric analysis of distributed firm real-time systems: A case study. - Thi Thieu Hoa Le; Luigi Palopoli 002; Roberto Passerone; Yusi Ramadian; Alessandro Cimatti (ETFA, 2010)

Verifying SystemC: A software model checking approach. - Alessandro Cimatti; Andrea Micheli; Iman Narasamdya; Marco Roveri (FMCAD, 2010)

Applying SMT in symbolic execution of microcode. - Anders Franzén; Alessandro Cimatti; Alexander Nadel; Roberto Sebastiani; Jonathan Shalev (FMCAD, 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)

SMT-Based Software Model Checking. - Alessandro Cimatti (SPIN, 2010)

Satisfiability Modulo the Theory of Costs: Foundations and Applications. - Alessandro Cimatti; Anders Franzén; Alberto Griggio; Roberto Sebastiani; Cristian Stenico (TACAS, 2010)

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

Efficient generation of craig interpolants in satisfiability modulo theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (ACM Trans. Comput. Log., 2010)

Kratos - A Software Model Checker for SystemC. - Alessandro Cimatti; Alberto Griggio; Andrea Micheli; Iman Narasamdya; Marco Roveri (CAV, 2011)

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)

A Comprehensive Approach to On-Board Autonomy Verification and Validation. - Marco Bozzano; Alessandro Cimatti; Marco Roveri; Andrei Tchaltsev (IJCAI, 2011)

An Analytic Evaluation of SystemC Encodings in Promela. - Daniele Campana; Alessandro Cimatti; Iman Narasamdya; Marco Roveri (SPIN, 2011)

Boosting Lazy Abstraction for SystemC with Partial Order Reduction. - Alessandro Cimatti; Iman Narasamdya; Marco Roveri (TACAS, 2011)

Safety, Dependability and Performance Analysis of Extended AADL Models. - Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll 001; Marco Roveri (Comput. J., 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)

Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Roberto Sebastiani (J. Artif. Intell. Res., 2011)

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

Symbolic Synthesis of Observability Requirements for Diagnosability. - Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Xavier Olive (AAAI, 2012)

Solving Temporal Problems Using SMT: Weak Controllability. - Alessandro Cimatti; Andrea Micheli; Marco Roveri (AAAI, 2012)

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

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 (CAV, 2012)

Software Model Checking via IC3. - Alessandro Cimatti; Alberto Griggio (CAV, 2012)

Solving Temporal Problems Using SMT: Strong Controllability. - Alessandro Cimatti; Andrea Micheli; Marco Roveri (CP, 2012)

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

Application of SMT solvers to hybrid system verification. - Alessandro Cimatti (FMCAD, 2012)

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

Verification of parametric system designs. - Alessandro Cimatti; Iman Narasamdya; Marco Roveri (FMCAD, 2012)

Software Model Checking with Explicit Scheduler and Symbolic Threads - Alessandro Cimatti; Iman Narasamdya; Marco Roveri (Log. Methods Comput. Sci., 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)

Timelines with Temporal Uncertainty. - Alessandro Cimatti; Andrea Micheli; Marco Roveri (AAAI, 2013)

SMT-Based Software Model Checking - Explicit Scheduler, Symbolic Threads. - Alessandro Cimatti (ATVA, 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)

Efficient Analysis of Reliability Architectures via Predicate Abstraction. - Marco Bozzano; Alessandro Cimatti; Cristian Mattarei (Haifa Verification Conference, 2013)

Automated Analysis of Reliability Architectures. - Marco Bozzano; Alessandro Cimatti; Cristian Mattarei (ICECCS, 2013)

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

A Modular Approach to MaxSAT Modulo Theories. - Alessandro Cimatti; Alberto Griggio; Bastiaan Joost Schaafsma; Roberto Sebastiani (SAT, 2013)

The MathSAT5 SMT Solver. - Alessandro Cimatti; Alberto Griggio; Bastiaan Joost Schaafsma; Roberto Sebastiani (TACAS, 2013)

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

Software Model Checking SystemC. - Alessandro Cimatti; Iman Narasamdya; Marco Roveri (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2013)

Using Timed Game Automata to Synthesize Execution Strategies for Simple Temporal Networks with Uncertainty. - Alessandro Cimatti; Luke Hunsberger; Andrea Micheli; Marco Roveri (AAAI, 2014)

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)

Towards Pareto-optimal parameter synthesis for monotonic cost functions. - Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Marco Gario; Alberto Griggio (FMCAD, 2014)

An Integrated Process for FDIR Design in Aerospace. - Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Régis De Ferluc; Marco Gario; Andrea Guiotto; Yuri Yushtein (IMBSA, 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)

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 (TIME, 2014)

Automated Planning and Model Checking (Dagstuhl Seminar 14482). - Alessandro Cimatti; Stefan Edelkamp; Maria Fox 001; Daniele Magazzeni; Erion Plaku (Dagstuhl Reports, 2014)

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

Spacecraft early design validation using formal methods. - Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Panagiotis Katsaros; Konstantinos Mokos; Viet Yen Nguyen; Thomas Noll 001; Bart Postma; Marco Roveri (Reliab. Eng. Syst. Saf., 2014)

SMT-Based Validation of Timed Failure Propagation Graphs. - Marco Bozzano; Alessandro Cimatti; Marco Gario; Andrea Micheli (AAAI, 2015)

Strong Temporal Planning with Uncontrollable Durations: A State-Space Approach. - Alessandro Cimatti; Andrea Micheli; Marco Roveri (AAAI, 2015)

Formal Verification of Infinite-State BIP Models. - Simon Bliudze; Alessandro Cimatti; Mohamad Jaber 001; Sergio Mover; Marco Roveri; Wajeb Saab; Qiang Wang 020 (ATVA, 2015)

Efficient Anytime Techniques for Model-Based Safety Analysis. - Marco Bozzano; Alessandro Cimatti; Alberto Griggio; Cristian Mattarei (CAV (1), 2015)

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)

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)

An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty. - Alessandro Cimatti; Andrea Micheli; Marco Roveri (Artif. Intell., 2015)

Solving strong controllability of temporal problems with uncertainty using SMT. - Alessandro Cimatti; Andrea Micheli; Marco Roveri (Constraints An Int. J., 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)

Automated Verification and Tightening of Failure Propagation Models. - Benjamin Bittner; Marco Bozzano; Alessandro Cimatti; Gianni Zampedri (AAAI, 2016)

Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies. - Alessandro Cimatti; Andrea Micheli; Marco Roveri (AAAI, 2016)

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)

Verilog2SMV: A tool for word-level verification. - Ahmed Irfan; Alessandro Cimatti; Alberto Griggio; Marco Roveri; Roberto Sebastiani (DATE, 2016)

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

From Electrical Switched Networks to Hybrid Automata. - Alessandro Cimatti; Sergio Mover; Mirko Sessa (FM, 2016)

Automated Synthesis of Timed Failure Propagation Graphs. - Benjamin Bittner; Marco Bozzano; Alessandro Cimatti (IJCAI, 2016)

SC2: Satisfiability Checking Meets Symbolic Computation - (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CICM, 2016)

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

The xSAP Safety Analysis Platform. - Benjamin Bittner; Marco Bozzano; Roberto Cavada; Alessandro Cimatti; Marco Gario; Alberto Griggio; Cristian Mattarei; Andrea Micheli; Gianni Zampedri (TACAS, 2016)

Dynamic controllability via Timed Game Automata. - Alessandro Cimatti; Luke Hunsberger; Andrea Micheli; Roberto Posenato; Marco Roveri (Acta Informatica, 2016)

Satisfiability checking and symbolic computation. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (ACM Commun. Comput. Algebra, 2016)

Satisfiability Checking meets Symbolic Computation (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CoRR, 2016)

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

Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic. - Alessandro Cimatti; Andrea Micheli; Marco Roveri (AAAI, 2017)

SC-square: when Satisfiability Checking and Symbolic Computation join forces. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Vijay Ganesh 001; Alberto Griggio; et al. (ARCADE@CADE, 2017)

Satisfiability Modulo Transcendental Functions via Incremental Linearization. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (CADE, 2017)

SMT-based analysis of switching multi-domain linear Kirchhoff networks. - Alessandro Cimatti; Sergio Mover; Mirko Sessa (FMCAD, 2017)

Timed Failure Propagation Analysis for Spacecraft Engineering: The ESA Solar Orbiter Case Study. - Benjamin Bittner; Marco Bozzano; Alessandro Cimatti (IMBSA, 2017)

Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (TACAS (1), 2017)

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

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 (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)

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (SAT, 2018)

Symbolic execution with existential second-order constraints. - Sergey Mechtaev; Alberto Griggio; Alessandro Cimatti; Abhik Roychoudhury (ESEC/SIGSOFT FSE, 2018)

Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (SYNASC, 2018)

Strong temporal planning with uncontrollable durations. - Alessandro Cimatti; Minh Do; Andrea Micheli; Marco Roveri; David E. Smith 001 (Artif. Intell., 2018)

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

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (ACM Trans. Comput. Log., 2018)

Robustness Envelopes for Temporal Plans. - Michael Cashmore; Alessandro Cimatti; Daniele Magazzeni; Andrea Micheli; Parisa Zehtabi (AAAI, 2019)

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)

Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. - Ahmed Irfan; Alessandro Cimatti; Alberto Griggio; Marco Roveri; Roberto Sebastiani (SC-square@SIAM AG, 2019)

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

Towards Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans. - Michael Cashmore; Alessandro Cimatti; Daniele Magazzeni; Andrea Micheli; Parisa Zehtabi (CoRR, 2019)

Formal reliability analysis of redundancy architectures. - Marco Bozzano; Alessandro Cimatti; Cristian Mattarei (Formal Aspects Comput., 2019)

Temporal Planning with Intermediate Conditions and Effects. - Alessandro Valentini 001; Andrea Micheli; Alessandro Cimatti (AAAI, 2020)

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

Computation of the Transient in Max-Plus Linear Systems via SMT-Solving. - Alessandro Abate; Alessandro Cimatti; Andrea Micheli; Muhammad Syifa'ul Mufid (FORMATS, 2020)

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 (ISoLA (3), 2020)

Synthesis of P-Stable Abstractions. - Anna Becchi; Alessandro Cimatti; Enea Zaffanella (SEFM, 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)

Automatic Design Space Exploration of Redundant Architectures. - Antonio Tierno; Giuliano Turri; Alessandro Cimatti; Roberto Passerone (ApplePies, 2021)

Automatic Discovery of Fair Paths in Infinite-State Transition Systems. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago (ATVA, 2021)

Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. - Alessandro Cimatti; Alberto Griggio; Gianluca Redondi (CADE, 2021)

Efficient SMT-Based Analysis of Failure Propagation. - Marco Bozzano; Alessandro Cimatti; Anthony Fernandes Pires; Alberto Griggio; Martin Jonás; Greg Kimberly (CAV (2), 2021)

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

SMT-Based Model Checking of Max-Plus Linear Systems. - Muhammad Syifa'ul Mufid; Andrea Micheli; Alessandro Abate; Alessandro Cimatti (CONCUR, 2021)

Optimization Modulo Non-linear Arithmetic via Incremental Linearization. - Filippo Bigarella; Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Martin Jonás; Marco Roveri; Roberto Sebastiani; Patrick Trentin (FroCoS, 2021)

Reverse engineering with P-stable Abstractions. - Anna Becchi; Alessandro Cimatti; Enea Zaffanella (OVERLAY@GandALF, 2021)

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

Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans. - Michael Cashmore; Alessandro Cimatti; Daniele Magazzeni; Andrea Micheli; Parisa Zehtabi (TIME, 2021)

Proving the Existence of Fair Paths in Infinite-State Systems. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago (VMCAI, 2021)

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

Model-based Safety Assessment of a Triple Modular Generator with xSAP. - Marco Bozzano; Alessandro Cimatti; Marco Gario; David Jones; Cristian Mattarei (Formal Aspects Comput., 2021)

A Comprehensive Approach to On-board Autonomy Verification and Validation. - Marco Bozzano; Alessandro Cimatti; Marco Roveri (ACM Trans. Intell. Syst. Technol., 2021)

Deciding Unsolvability in Temporal Planning under Action Non-Self-Overlapping. - Stefan Panjkovic; Andrea Micheli; Alessandro Cimatti (AAAI, 2022)

Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test. - Alessandro Cimatti; Alberto Griggio; Enrico Lipparini; Roberto Sebastiani (ATVA, 2022)

Verification of SMT Systems with Quantifiers. - Alessandro Cimatti; Alberto Griggio; Gianluca Redondi (ATVA, 2022)

Abstraction Modulo Stability for Reverse Engineering. - Anna Becchi; Alessandro Cimatti (CAV (1), 2022)

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

Symbolic Encoding of Reliability for the Design of Redundant Architectures. - Antonio Tierno; Giuliano Turri; Alessandro Cimatti; Roberto Passerone (ICPS, 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)

Analysis of Cyclic Fault Propagation via ASP. - Marco Bozzano; Alessandro Cimatti; Alberto Griggio; Martin Jonás; Greg Kimberly (LPNMR, 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)

Formal Design and Validation of an Automatic Train Operation Control System. - 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 (RSSRail, 2022)

A Formal IDE for Railways: Research Challenges. - Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Angelo Susi (SEFM Workshops, 2022)

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

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 (TACAS (1), 2022)

Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation. - Marco Bozzano; Alessandro Cimatti; Alberto Griggio; Martin Jonás (TACAS (2), 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)

LTL falsification in infinite-state systems. - Alessandro Cimatti; Alberto Griggio; Enrico Magnago (Inf. Comput., 2022)

Semi-ProtoPNet Deep Neural Network for the Classification of Defective Power Grid Distribution Structures. - Stéfano Frizzo Stefenon; Gurmail Singh; Kin Choong Yow 001; Alessandro Cimatti (Sensors, 2022)

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

Towards Automatic Digitalization of Railway Engineering Schematics. - Stéfano Frizzo Stefenon; Marco Cristoforetti; Alessandro Cimatti (AI*IA, 2023)

Searching for i-Good Lemmas to Accelerate Safety Model Checking. - Yechuan Xia; Anna Becchi; Alessandro Cimatti; Alberto Griggio; Jianwen Li; Geguang Pu (CAV (2), 2023)

Set-Based Invariants over Polynomial Systems. - Alberto Casagrande; Alessandro Cimatti; Luca Dorigo; Carla Piazza; Stefano Tonetta (CILC, 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)

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)

Formal Analysis and Verification of Max-Plus Linear Systems. - Muhammad Syifa'ul Mufid; Andrea Micheli; Alessandro Abate; Alessandro Cimatti (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)

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

Testing the Migration from Analog to Software-Based Railway Interlocking Systems. - Anna Becchi; Alessandro Cimatti; Giuseppe Scaglione (CAV (2), 2024)

Avoiding the Shoals - A New Approach to Liveness Checking. - Yechuan Xia; Alessandro Cimatti; Alberto Griggio; Jianwen Li (CAV (1), 2024)

SMT-Based Repair of Disjunctive Temporal Networks with Uncertainty: Strong and Weak Controllability. - Ajdin Sumic; Alessandro Cimatti; Andrea Micheli; Thierry Vidal (CPAIOR (2), 2024)

Inferring Sensor Placement Using Critical Pairs and Satisfiability Modulo Theory. - Alexander Diedrich; René Heesch; Marco Bozzano; Björn Ludwig; Alessandro Cimatti; Oliver Niggemann (DX, 2024)

Summary of "A Lazy Approach to Neural Numerical Planning with Control Parameters" (Extended Abstract). - René Heesch; Alessandro Cimatti; Jonas Ehrhardt; Alexander Diedrich; Oliver Niggemann (DX, 2024)

A Lazy Approach to Neural Numerical Planning with Control Parameters. - René Heesch; Alessandro Cimatti; Jonas Ehrhardt; Alexander Diedrich; Oliver Niggemann (ECAI, 2024)

Towards Verification Modulo Theories of Asynchronous Systems via Abstraction Refinement. - Gianluca Redondi; Alessandro Cimatti; Alberto Griggio (FMCAD, 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)

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 Analysis of Algorithmic Requirements. - Lorenzo Cappelletti; Roberto Cavada; Alessandro Cimatti; Marco Keppel (ISoLA (3), 2024)

Model-Based Testing of Railway Interlocking Systems. - Alessandro Cimatti; Shaker Khandaker; Fitsum Meshesha Kifetew; Lorenzo Leone; Davide Prandi; Giuseppe Scaglione; Angelo Susi; Orazio Turboli (ISoLA (5), 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)

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)

Introducing Interdependent Simple Temporal Networks with Uncertainty for Multi-Agent Temporal Planning. - Ajdin Sumic; Thierry Vidal; Andrea Micheli; Alessandro Cimatti (TIME, 2024)

Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking. - Alessandro Cimatti; Alberto Griggio; Gianluca Redondi (CoRR, 2024)

Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis (Dagstuhl Seminar 24031). - Alessandro Cimatti; Ingo Pill; Alexander Diedrich (Dagstuhl Reports, 2024)

Invariant Checking for SMT-Based Systems with Quantifiers. - Gianluca Redondi; Alessandro Cimatti; Alberto Griggio; Kenneth L. McMillan (ACM Trans. Comput. Log., 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)

Opportunistic (Re)planning for Long-Term Deep-Ocean Inspection: An Autonomous Underwater Architecture. - Elisa Tosello; Paolo Bonel; Alberto Buranello; Marco Carraro; Alessandro Cimatti; Lorenzo Granelli; Stefan Panjkovic; Andrea Micheli (IEEE Robotics Autom. Mag., 2024)

Artifact for CAV'24 paper "Avoiding the Shoals - A New Approach to Liveness Checking". - Yechuan Xia; Alessandro Cimatti; Alberto Griggio; Jianwen Li (Zenodo, 2024)

P-stable abstractions of hybrid systems. - Anna Becchi; Alessandro Cimatti; Enea Zaffanella (Softw. Syst. Model., 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)

Automated Parameterized Verification of a Railway Protection System with Dafny. - Roberto Cavada; Alessandro Cimatti; Alberto Griggio; Christian Lidström; Gianluca Redondi; Giuseppe Scaglione; Matteo Tessi; Dylan Trenti (CAV (4), 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)

Automatic digitalization of railway interlocking systems engineering drawings based on hybrid machine learning methods. - Stéfano Frizzo Stefenon; Marco Cristoforetti; Alessandro Cimatti (Expert Syst. Appl., 2025)

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

Formal methods in industrial critical systems. - Alessandro Cimatti; Laura Titolo (Int. J. Softw. Tools Technol. Transf., 2025)

Abstraction Modulo Stability. - Anna Becchi; Alessandro Cimatti (Formal Methods Syst. Des., 2025)

Conditional diffusion to enhance performance of object detection in unbalanced data engineering drawings. - Stéfano Frizzo Stefenon; Marco Cristoforetti; Alessandro Cimatti (Neural Comput. Appl., 2025)