Cimatti, Alessandro; Geatti, Luca; Gigante, Nicola; Montanari, Angelo; Tonetta, Stefano A first-order logic characterization of safety and co-safety languages. (English) Zbl 07731941 Log. Methods Comput. Sci. 19, No. 3, Paper No. 13, 29 p. (2023). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{A. Cimatti} et al., Log. Methods Comput. Sci. 19, No. 3, Paper No. 13, 29 p. (2023; Zbl 07731941) Full Text: DOI arXiv
Cimatti, Alessandro; Geatti, Luca; Gigante, Nicola; Montanari, Angelo; Tonetta, Stefano A first-order logic characterisation of safety and co-safety languages. (English) Zbl 07793032 Bouyer, Patricia (ed.) et al., Foundations of software science and computation structures. 25th international conference, FOSSACS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2–7, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13242, 244-263 (2022). MSC: 68Nxx 68Qxx PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 13242, 244--263 (2022; Zbl 07793032) Full Text: DOI
Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Roveri, Marco; Tonetta, Stefano Verification Modulo theories. (English) Zbl 07757158 Form. Methods Syst. Des. 60, No. 3, 452-481 (2022). MSC: 68-XX PDFBibTeX XMLCite \textit{A. Cimatti} et al., Form. Methods Syst. Des. 60, No. 3, 452--481 (2022; Zbl 07757158) Full Text: DOI OA License
Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca Verification of SMT systems with quantifiers. (English) Zbl 1522.68303 Bouajjani, Ahmed (ed.) et al., Automated technology for verification and analysis. 20th international symposium, ATVA 2022, virtual event, October 25–28, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13505, 154-170 (2022). MSC: 68Q60 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 13505, 154--170 (2022; Zbl 1522.68303) Full Text: DOI
Cimatti, Alessandro; Griggio, Alberto; Lipparini, Enrico; Sebastiani, Roberto Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test. (English) Zbl 1522.68716 Bouajjani, Ahmed (ed.) et al., Automated technology for verification and analysis. 20th international symposium, ATVA 2022, virtual event, October 25–28, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13505, 137-153 (2022). MSC: 68V15 55M25 90C30 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 13505, 137--153 (2022; Zbl 1522.68716) Full Text: DOI
Cimatti, Alessandro; Tian, Chun; Tonetta, Stefano Assumption-based runtime verification. (English) Zbl 07683090 Form. Methods Syst. Des. 60, No. 2, 277-324 (2022). MSC: 68-XX PDFBibTeX XMLCite \textit{A. Cimatti} et al., Form. Methods Syst. Des. 60, No. 2, 277--324 (2022; Zbl 07683090) Full Text: DOI
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico LTL falsification in infinite-state systems. (English) Zbl 07629158 Inf. Comput. 289, Part A, Article ID 104977, 43 p. (2022). MSC: 68Qxx PDFBibTeX XMLCite \textit{A. Cimatti} et al., Inf. Comput. 289, Part A, Article ID 104977, 43 p. (2022; Zbl 07629158) Full Text: DOI
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico Automatic discovery of fair paths in infinite-state transition systems. (English) Zbl 1497.68290 Hou, Zhe (ed.) et al., Automated technology for verification and analysis. 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12971, 32-47 (2021). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 12971, 32--47 (2021; Zbl 1497.68290) Full Text: DOI
Mover, Sergio; Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Tonetta, Stefano Implicit semi-algebraic abstraction for polynomial dynamical systems. (English) Zbl 1493.68217 Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12759, 529-551 (2021). MSC: 68Q60 03B70 34A34 PDFBibTeX XMLCite \textit{S. Mover} et al., Lect. Notes Comput. Sci. 12759, 529--551 (2021; Zbl 1493.68217) Full Text: DOI
Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca Universal invariant checking of parametric systems with quantifier-free SMT reasoning. (English) Zbl 07437076 Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 131-147 (2021). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 12699, 131--147 (2021; Zbl 07437076) Full Text: DOI
Cimatti, Alessandro; Griggio, Alberto; Magnago, Enrico Proving the existence of fair paths in infinite-state systems. (English) Zbl 1472.68085 Henglein, Fritz (ed.) et al., Verification, model checking, and abstract interpretation. 22nd international conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12597, 104-126 (2021). MSC: 68Q60 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 12597, 104--126 (2021; Zbl 1472.68085) Full Text: DOI
Bozzano, Marco; Cimatti, Alessandro; Gario, Marco; Jones, David; Mattarei, Cristian Model-based safety assessment of a triple modular generator with xSAP. (English) Zbl 1511.68149 Formal Asp. Comput. 33, No. 2, 251-295 (2021). MSC: 68Q60 93-10 93C83 PDFBibTeX XMLCite \textit{M. Bozzano} et al., Formal Asp. Comput. 33, No. 2, 251--295 (2021; Zbl 1511.68149) Full Text: DOI
Cimatti, Alessandro; Geatti, Luca; Griggio, Alberto; Kimberly, Greg; Tonetta, Stefano Safe decomposition of startup requirements: verification and synthesis. (English) Zbl 1507.68180 Biere, Armin (ed.) et al., Tools and algorithms for the construction and analysis of systems. 26th international conference, TACAS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12078, 155-172 (2020). MSC: 68Q60 68Q45 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 12078, 155--172 (2020; Zbl 1507.68180) Full Text: DOI
Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. (English) Zbl 1452.68116 Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 58-75 (2017). MSC: 68Q60 68Q45 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 10205, 58--75 (2017; Zbl 1452.68116) Full Text: DOI arXiv
Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano Infinite-state invariant checking with IC3 and predicate abstraction. (English) Zbl 1368.68245 Form. Methods Syst. Des. 49, No. 3, 190-218 (2016). MSC: 68Q60 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Form. Methods Syst. Des. 49, No. 3, 190--218 (2016; Zbl 1368.68245) Full Text: DOI
Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano HRELTL: a temporal logic for hybrid systems. (English) Zbl 1332.68139 Inf. Comput. 245, 54-71 (2015). MSC: 68Q60 03B44 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Inf. Comput. 245, 54--71 (2015; Zbl 1332.68139) Full Text: DOI
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano Quantifier-free encoding of invariants for hybrid systems. (English) Zbl 1317.68111 Form. Methods Syst. Des. 45, No. 2, 165-188 (2014). MSC: 68Q60 93C30 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Form. Methods Syst. Des. 45, No. 2, 165--188 (2014; Zbl 1317.68111) Full Text: DOI
Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano SMT-based scenario verification for hybrid systems. (English) Zbl 1284.03216 Form. Methods Syst. Des. 42, No. 1, 46-66 (2013). MSC: 03D05 68Q60 68T20 68Q45 03B44 03D78 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Form. Methods Syst. Des. 42, No. 1, 46--66 (2013; Zbl 1284.03216) Full Text: DOI
Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco Boosting lazy abstraction for SystemC with partial order reduction. (English) Zbl 1316.68072 Abdulla, Parosh Aziz (ed.) et al., Tools and algorithms for the construction and analysis of systems. 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19834-2/pbk). Lecture Notes in Computer Science 6605, 341-356 (2011). MSC: 68Q60 68-04 PDFBibTeX XMLCite \textit{A. Cimatti} et al., Lect. Notes Comput. Sci. 6605, 341--356 (2011; Zbl 1316.68072) Full Text: DOI
Rakamarić, Zvonimir; Bruttomesso, Roberto; Hu, Alan J.; Cimatti, Alessandro Verifying heap-manipulating programs in an SMT framework. (English) Zbl 1141.68484 Namjoshi, Kedar S. (ed.) et al., Automated technology for verification and analysis. 5th international symposium, ATVA 2007 Tokyo, Japan, October 22–25, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75595-1/pbk). Lecture Notes in Computer Science 4762, 237-252 (2007). MSC: 68Q60 68N30 68T15 PDFBibTeX XMLCite \textit{Z. Rakamarić} et al., Lect. Notes Comput. Sci. 4762, 237--252 (2007; Zbl 1141.68484) Full Text: DOI