Publications
-
Cavada Roberto; Cimatti Alessandro; Mover Sergio; Sessa Mirko; Cadavero Giuseppe; Scaglione Giuseppe,
Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks, Proceedings of 2018 Formal Methods in Computer Aided Design, FMCAD 2018, 2018, DOI: 10.23919/FMCAD.2018.8603007
-
Cimatti Alessandro; Ghilardi Silvio; Ranise Silvio,
Model checking: teoria ed applicazioni, Le direzioni della ricerca logica in Italia 2, 2018, pp. 141-193, Edizioni ETS
-
Mechtaev Sergey; Griggio Alberto; Cimatti Alessandro; Roychoudhury Abhik,
Symbolic execution with existential second-order constraints, Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, 2018, pp. 389-399, DOI: 10.1145/3236024.3236049
-
Griggio Alberto; Roveri Marco; Tonetta Stefano,
Certifying Proofs for LTL Model Checking, Formal Methods in Computer-Aided Design, FMCAD 2018, 2018, pp. 225-233
-
Cimatti Alessandro; Delong Rance; Stojic Ivan; Tonetta Stefano,
Towards Adaptive MILS Systems: Model-Based Design, Verification And Run-Time Adaptation, 2018, DOI: 10.5281/zenodo.1306063
-
Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto,
Incremental Linearization: A practical approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions, Proceedings of 2018 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018, DOI: 10.1109/SYNASC.2018.00016
-
Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto,
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF, Tools and Algorithms for the Construction and Analysis of Systems, vol. 10205, 2017, pp. 58-75, DOI: 10.1007/978-3-662-54577-5_4
-
Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto,
Satisfiability Modulo Transcendental Functions via Incremental Linearization, Automated Deduction – CADE 26, vol. 10395, 2017, pp. 95-113, DOI: 10.1007/978-3-319-63046-5_7
-
Cimatti Alessandro; Micheli Andrea; Roveri Marco,
Validating Domains and Plans for Temporal Planning via Encoding into Infinite-State Linear Temporal Logic, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, 2017, pp. 3547-3554, AAAI Press
-
Cimatti Alessandro; Mover Sergio; Sessa Mirko,
SMT-based analysis of switching multi-domain linear Kirchhoff networks, Proceedings of Formal Methods in Computer Aided Design (FMCAD 2017), 2017, pp. 188-195, DOI: 10.23919/FMCAD.2017.8102259
-
Bittner Benjamin; Bozzano Marco; Cimatti Alessandro,
Timed Failure Propagation Analysis for Spacecraft Engineering: The ESA Solar Orbiter Case Study, Proceedings of International Symposium on Model-Based Safety and Assessment, vol. 10437, 2017, pp. 255-271, DOI: 10.1007/978-3-319-64119-5_17, Springer
-
Bozzano Marco; Papadopoulos Yiannis,
Model-Based Safety and Assessment, vol. 10437, 2017, DOI: 10.1007/978-3-319-64119-5, Springer
-
Tonetta Stefano; Schoitsch Erwin; Bitsch Friedemann,
Computer Safety, Reliability, and Security - SAFECOMP 2017 Workshops, ASSURE, DECSoS, SASSUR, TELERISE, and TIPS, Trento, Italy, September 12, 2017, Proceedings, vol. 10489, 2017, DOI: 10.1007/978-3-319-66284-8, Springer
-
Tonetta Stefano; Schoitsch Erwin; Bitsch Friedemann,
Computer Safety, Reliability, and Security - 36th International Conference, SAFECOMP 2017, Trento, Italy, September 13-15, 2017, Proceedings, vol. 10488, 2017, DOI: 10.1007/978-3-319-66266-4, Springer
-
Tonetta Stefano,
Linear-time Temporal Logic with Event Freezing Functions, Proceedings Eighth International Symposium on Games, Automata, Logicsand Formal Verification, GandALF 2017, vol. 256, 2017, pp. 195-209, DOI: 10.4204/EPTCS.256.14
-
Artuso Stefano; Cristoforetti Luca; Falavigna Giuseppe Daniele; Gretter Roberto; Mana Nadia; Schiavo Gianluca,
A System for Assessing Children Reading at School, Proceedings of the Seventh ISCA workshop on Speech and Language Technology in Education 2017, 2017, pp. 115-120
-
Fauri Davide; Dos Santos Daniel Ricardo; Costante Elisa; den Hartog Jerry; Etalle Sandro; Tonetta Stefano,
From System Specification to Anomaly Detection (and back), Proceedings of the 2017 Workshop on Cyber-Physical Systems Securityand PrivaCy, 2017, pp. 13-24, DOI: 10.1145/3140241.3140250, ACM
-
Bozzano Marco; Bruintjes Harold; Cimatti Alessandro; Katoen Joost-Pieter; Noll Thomas; Tonetta Stefano,
Formal Methods for Aerospace Systems, Cyber-Physical System Design from an Architecture Analysis Viewpoint, 2017, pp. 133-159, Springer
-
Bozzano Marco,
Causality and Temporal Dependencies in the Design of Fault Management Systems, Proceedings 2nd International Workshop on Causal Reasoning for Embedded and safety-critical Systems Technologies (CREST 2017), in «ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE», vol. 259, 2017, pp. 39-46, ISSN: 2075-2180
-
Griggio Alberto; Rümmer Philipp,
Preface to special issue on satisfiability modulo theories, Formal Methods in System Design, vol. 51, 2017, pp. 431-432, DOI: 10.1007/s10703-017-0308-5
-
Bittner Benjamin; Bozzano Marco; Cavada Roberto; Cimatti Alessandro; Gario Marco Elio Gustavo; Griggio Alberto; Mattarei Cristian; Micheli Andrea; Zampedri Gianni,
The xSAP Safety Analysis Platform, Tools and Algorithms for the Construction and Analysis of Systems, vol. 9636, 2016, pp. 533-539, DOI: 10.1007/978-3-662-49674-9_31, Springer Berlin Heidelberg
-
Cimatti Alessandro; Hunsberger Luke; Micheli Andrea; Posenato Roberto; Roveri Marco,
Dynamic controllability via Timed Game Automata, in «ACTA INFORMATICA», 2016, pp. 1-42, DOI: 10.1007/s00236-016-0257-2, ISSN: 0001-5903
-
Bittner Benjamin; Bozzano Marco; Cimatti Alessandro; Zampedri Gianni,
Automated Verification and Tightening of Failure Propagation Models, Proceedings of the 30th AAAI Conference on Artificial Intelligence (AAAI 2016), 2016, pp. 907-913
-
Bittner Benjamin; Bozzano Marco; Cimatti Alessandro,
Automated Synthesis of Timed Failure Propagation Graphs, Proceedings of the 25th International Joint Conference on Artificial Intelligence, IJCAI, 2016, pp. 972-978
-
Ábrahám Erika; Abbott John; Becker Bernd; Bigatti Anna M.; Brain Martin; Buchberger Bruno; Cimatti Alessandro; Davenport James H.; England Matthew; Fontaine Pascal; Forrest Stephen; Griggio Alberto; Kroening Daniel; Seiler Werner M.; Sturm Thomas,
SC^2: Satisfiability Checking Meets Symbolic Computation, Intelligent Computer Mathematics - 9th International Conference, CICM 2016, vol. 9791, 2016, pp. 28-43, DOI: 10.1007/978-3-319-42547-4_3
-
Jakub Daniel; Cimatti Alessandro; Griggio Alberto; Tonetta Stefano; Mover Sergio,
Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations, Computer Aided Verification - 28th International Conference, CAV 2016, vol. 9779, 2016, pp. 271-291, DOI: 10.1007/978-3-319-41528-4_15
-
Irfan Ahmed; Cimatti Alessandro; Griggio Alberto; Roveri Marco; Sebastiani Roberto,
Verilog2SMV: A Tool for Word-level Verification, Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016, 2016, pp. 1156-1159, DOI: 10.3850/9783981537079_0765
-
Cimatti Alessandro; Micheli Andrea; Roveri Marco,
Dynamic Controllability of Disjunctive Temporal Networks: Validation and Synthesis of Executable Strategies, Proceedings of the Thirtieth AAAI}Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA, 2016, pp. 3116-3122
-
Gario Marco Elio Gustavo; Cimatti Alessandro; Mattarei Cristian; Tonetta Stefano; Rozier Kristin Yvonne,
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration, Computer Aided Verification - 28th International Conference CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, vol. 9780, 2016, pp. 3-22, DOI: 10.1007/978-3-319-41540-6_1
-
Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano,
A Lazy Approach to Temporal Epistemic Logic Model Checking, Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, 2016, pp. 1218-1226, International Foundation for Autonomous Agents and Multiagent Systems
-
Christophe Limbrée; Quentin Cappart; Charles Pecheur; Tonetta Stefano,
Verification of Railway Interlocking - Compositional Approach with OCRA, Reliability, Safety, and Security of Railway Systems. Modelling, Analysis,Verification, and Certification - First International Conference,RSSRail 2016, Paris, France, June 28-30, 2016, Proceedings, vol. 9707, 2016, pp. 134-149, DOI: 10.1007/978-3-319-33951-1_10, Springer
-
Victor Bos; Harold Bruintjes; Tonetta Stefano,
Catalogue of System and Software Properties, Computer Safety, Reliability, and Security - 35th International Conference,SAFECOMP 2016, Proceedings, vol. 9922, 2016, pp. 88-101, DOI: 10.1007/978-3-319-45477-1_8, Springer
-
Cimatti Alessandro; Demasi Ramiro Adrian; Tonetta Stefano,
Tightening a Contract Refinement, Software Engineering and Formal Methods - 14th International Conference,SEFM 2016, Held as Part of STAF 2016, Vienna, Austria, July 4-8,2016, Proceedings, vol. 9763, 2016, pp. 386-402, DOI: 10.1007/978-3-319-41591-8_26, Springer
-
Cimatti Alessandro; Mover S.; Sessa Mirko,
From Electrical Switched Networks to Hybrid Automata, Proceedings of the 21st International Symposium on Formal Methods, FM 2016, vol. 9995, 2016, pp. 164-181, DOI: 10.1007/978-3-319-48989-6_11
-
Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano,
Infinite-state invariant checking with IC3 and predicate abstraction, in «FORMAL METHODS IN SYSTEM DESIGN», 2016, DOI: 10.1007/s10703-016-0257-4, ISSN: 0925-9856
-
Cavada Roberto; Cimatti Alessandro; Crema Luigi; Roccabruna Mattia; Tonetta Stefano,
Model-Based Design of an Energy-System Embedded Controller Using Taste, Proceedings of FM 2016: Formal Methods 21st International Symposium, vol. 9995, 2016, pp. 741-747, DOI: 10.1007/978-3-319-48989-6_45
-
Ábrahám E.; Fontaine P.; Forrest S.; Griggio A.; Kroening D.; Seiler W. M.; Sturm T.; Abbott J.; Becker B.; Bigatti A. M.; Brain M.; Buchberger B.; Cimatti A.; Davenport J. H.; England M.,
Satisfiability checking and symbolic computation, in «ACM COMMUNICATIONS IN COMPUTER ALGEBRA», vol. 50, n. 4, 2016, pp. 145-147, DOI: 10.1145/3055282.3055285, ISSN: 1932-2240
-
Cimatti Alessandro; Micheli Andrea; Roveri Marco,
Solving strong controllability of temporal problems with uncertainty using SMT, in «CONSTRAINTS», vol. 20, 2015, pp. 7-29, DOI: 10.1007/s10601-014-9167-5, ISSN: 1383-7133
-
Cimatti Alessandro; Tonetta Stefano,
Contracts-refinement proof system for component-based embedded systems, in «SCIENCE OF COMPUTER PROGRAMMING», 2015, DOI: 10.1016/j.scico.2014.06.011, ISSN: 0167-6423
-
Bozzano Marco; Cimatti Alessandro; Oleg Lisagor; Mattarei Cristian; Mover Sergio; Roveri Marco; Tonetta Stefano,
Safety Assessment of AltaRica Models via Symbolic Model Checking, in «SCIENCE OF COMPUTER PROGRAMMING», vol. 98, 2015, pp. 464-483, DOI: 10.1016/j.scico.2014.06.003, ISSN: 0167-6423
-
Cimatti Alessandro; Micheli Andrea; Roveri Marco,
Strong Temporal Planning with Uncontrollable Durations: a State-Space Approach, Proceedings of the 29th AAAI Conference on Artificial Intelligence, 2015, AAAI Press
-
Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Micheli Andrea,
SMT-based Validation of Timed Failure Propagation Graphs, Proceedings of the 29th AAAI Conference on Artificial Intelligence, 2015, AAAI Press
-
Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano,
HYCOMP - an SMT-based model checker for hybrid systems, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, vol. 9035, 2015, pp. 52-67, DOI: 10.1007/978-3-662-46681-0_4, Springer
-
Cimatti Alessandro; Micheli Andrea; Roveri Marco,
An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty, in «ARTIFICIAL INTELLIGENCE», vol. 224, 2015, pp. 1-27, DOI: 10.1016/j.artint.2015.03.002, ISSN: 0004-3702
-
Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano,
Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic, in «LOGICAL METHODS IN COMPUTER SCIENCE», vol. 11, n. 4, 2015, DOI: 10.2168/LMCS-11(4:4)2015, ISSN: 1860-5974
-
Griggio Alberto; Roveri Marco,
Comparing Different Variants of the IC3 Algorithm for Hardware Model Checking, in «IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS», 2015, pp. 1-1, DOI: 10.1109/TCAD.2015.2481869, ISSN: 0278-0070
-
Ravanelli Mirco; Cristoforetti Luca; Gretter Roberto; Pellin Marco; Sosi Alessandro; Omologo Maurizio,
The DIRHA-English corpus and related tasks for distant-speech recognition in domestic environments, Proceedings of 2015 IEEE Workshop on Automatic Speech Recognition and Understanding (ASRU), 2015, pp. 275-282, DOI: 10.1109/ASRU.2015.7404805, IEEE
-
Cimatti Alessandro; Roveri Marco; Tonetta Stefano,
HRELTL: A temporal logic for hybrid systems, in «INFORMATION AND COMPUTATION», vol. 245, 2015, pp. 54-71, DOI: 10.1016/j.ic.2015.06.006, ISSN: 0890-5401
-
Bozzano Marco; Cimatti Alessandro; Griggio Alberto; Mattarei Cristian,
Efficient Anytime Techniques for Model-Based Safety Analysis, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, vol. 9206, 2015, pp. 603-621, DOI: 10.1007/978-3-319-21690-4_41
-
Mattarei Cristian; Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano; Rozier Kristin Yvonne,
Comparing Different Functional Allocations in Automated Air Traffic Control Design, Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2015, 2015, pp. 112-119, IEEE