Publications

  1. Cimatti Alessandro; Do Minh; Micheli Andrea; Roveri Marco; Smith David E., Strong temporal planning with uncontrollable durations, in «ARTIFICIAL INTELLIGENCE», vol. 256, 2018, pp. 1-34, DOI: 10.1016/j.artint.2017.11.006, ISSN: 0004-3702
  2. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization, Proceedings of Theory and Applications of Satisfiability Testing – SAT 2018, vol. 10929, 2018, pp. 383-398, DOI: 10.1007/978-3-319-94144-8_23
  3. Cimatti Alessandro; Stojic Ivan; Tonetta Stefano, Formal Specification and Verification of Dynamic Parametrized Architectures, Formal Methods - 22nd International Symposium, FM 2018, Held asPart of the Federated Logic Conference, FloC 2018, Proceedings, vol. 10951, 2018, pp. 625-644, DOI: 10.1007/978-3-319-95582-7_37, Springer
  4. Cimatti Alessandro; Griggio Alberto; Irfan Ahmed; Roveri Marco; Sebastiani Roberto, Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions, in «ACM TRANSACTIONS ON COMPUTATIONAL LOGIC», vol. 19, n. 3, 2018, pp. 1-52, DOI: 10.1145/3230639, ISSN: 1529-3785
  5. 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
  6. 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
  7. 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
  8. Griggio Alberto; Roveri Marco; Tonetta Stefano, Certifying Proofs for LTL Model Checking, Formal Methods in Computer-Aided Design, FMCAD 2018, 2018, pp. 225-233
  9. 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
  10. 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
  11. 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
  12. 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
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. Á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
  23. 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
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. Á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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. Bliudze Simon; Cimatti Alessandro; Jaber Mohamad; Mover Sergio; Roveri Marco; Saab Wajeb; Wang Qiang, Formal Verification of Infinite-State BIP Models, Proceedings of ATVA, vol. 9364, 2015, pp. 326-343, DOI: 10.1007/978-3-319-24953-7, Springer
  45. Bozzano Marco; Cimatti Alessandro; Fernandes Pires Anthony; Jones D.; Kimberly G.; Petri T.; Robinson R.; Tonetta Stefano, Formal Design and Safety Analysis of AIR6110 Wheel Brake System, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, vol. 9206, 2015, pp. 518-535, DOI: 10.1007/978-3-319-21690-4_36
  46. Arts Thomas; Tonetta Stefano, Safely Using the AUTOSAR End-to-End Protection Library, Computer Safety, Reliability, and Security - 34th International Conference, SAFECOMP 2015 Delft, The Netherlands, September 23-25, 2015. Proceedings, vol. 9337, 2015, pp. 74-89, DOI: 10.1007/978-3-319-24255-2_7
  47. Cimatti Alessandro; Delong Rance; Marcantonio Davide; Tonetta Stefano, Combining MILS with Contract-Based Design for Safety and Security Requirements, Computer Safety, Reliability, and Security - SAFECOMP 2015 Workshops, ASSURE, DECSoS, ISSE, ReSA4CI, and SASSUR, Delft, The Netherlands, September 22, 2015, Proceedings, vol. 9338, 2015, pp. 264-276, DOI: 10.1007/978-3-319-24249-1_23
  48. Bozzano Marco; Cimatti Alessandro; Gario Marco Elio Gustavo; Tonetta Stefano, Formal Design of Fault Detection and Identification Components Using Temporal Epistemic Logic, TACAS 2014, LNCS 8413,, vol. 8413, 2014, pp. 326-340, Springer-Verlag
  49. Cimatti Alessandro; Mover Sergio; Tonetta Stefano, Quantifier-free encoding of invariants for hybrid systems, in «FORMAL METHODS IN SYSTEM DESIGN», vol. 45, n. 2, 2014, pp. 165-188, DOI: 10.1007/s10703-013-0202-8, ISSN: 0925-9856
  50. Cimatti Alessandro; Griggio Alberto; Mover Sergio; Tonetta Stefano, IC3 Modulo Theories via Implicit Predicate Abstraction, TACAS, vol. 8413, 2014, pp. 46-61, DOI: 10.1007/978-3-642-54862-8_4, Springer

Recent Posts