Software Engineering and Formal Methods

Disjoint Partial Enumeration without Blocking Clauses
Spallitta, Giuseppe; Sebastiani, Roberto; Biere, Armin in The 38th Annual AAAI Conference on Artificial Intelligence, Vancouver: AAAI press, In press. Proceedings of: AAAI24, Vancouver, 22/02/2024

Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Cimatti, Alessandro; Griggio, Alberto; Redondi, Gianluca in Dafny 2024, 2024. Proceedings of: POPL 2024, Londra, 14 Gennaio 2024. - Publication URL

P-stable abstractions of hybrid systems
Becchi, Anna; Cimatti, Alessandro; Zaffanella, Enea in SOFTWARE AND SYSTEMS MODELING, v. 2024, (2024). - DOI: 10.1007/s10270-023-01145-x

Effective prime factorization via quantum annealing by modular locally-structured embedding
Ding, Jingwen; Spallitta, Giuseppe; Sebastiani, Roberto in SCIENTIFIC REPORTS, v. 14, n. 1 (2024), p. 3518. - DOI: 10.1038/s41598-024-53708-7
[other topics: Quantum Information and Computing

Enhancing SMT-based Weighted Model Integration by structure awareness
Spallitta, G.; Masina, G.; Morettin, P.; Passerini, A.; Sebastiani, R. in ARTIFICIAL INTELLIGENCE, v. 328, (2024). - DOI: 10.1016/j.artint.2024.104067

Enumerating Disjoint Partial Models without Blocking Clauses
Spallitta, Giuseppe; Biere, Armin; Sebastiani, Roberto in Workshop on Counting and Sampling 2023, 2023. Proceedings of: WMC23, Alghero, 4th July 2023

Automatic Generation of Scenarios for System-level Simulation-based Verification of Autonomous Driving Systems
Goyal, Srajan; Griggio, Alberto; Kimblad, Jacob; Tonetta, Stefano in Fifth International Workshop on Formal Methods for Autonomous Systems (FMAS 2023), Waterloo, Australia: EPTCS, 2023, p. 113-129. - (ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE). Proceedings of: FMAS 2023, Lieden, Netherlands, 15th-16th November, 2023. - Publication URL . - DOI: 10.4204/EPTCS.395.8

Evaluating Heuristic Search Algorithms in Pathfinding: A Comprehensive Study on Performance Metrics and Domain Parameters
Kherrour, Aya; Robol, Marco; Roveri, Marco; Giorgini, Paolo in Electronic Proceedings in Theoretical Computer Science, 2023. Proceedings of: AREA woekshop, Krakow, Poland, 30th September- 4th October 2023

Searching for i-Good Lemmas to Accelerate Safety Model Checking
Xia, Y.; Becchi, A.; Cimatti, A.; Griggio, A.; Li, J.; Pu, G. in Computer Aided Verification - 35th International Conference, CAV, 2023, GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND: SPRINGER INTERNATIONAL PUBLISHING AG, 2023, p. 288-308. - ISBN: 978-3-031-37702-0. Proceedings of: CAV, Paris, France, 17-22 July 2023. - DOI: 10.1007/978-3-031-37703-7_14

SMT-Based Stability Verification of an Industrial Switched PI Control Systems
Basagiannis, Stylianos; Battista, Ludovico; Becchi, Anna; Cimatti, Alessandro; Giantamidis, Georgios; Mover, Sergio; Tacchella, Alberto; Tonetta, Stefano; Tsachouridis, Vassilios in 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2023, Porto, Portugal: IEEE, 2023, p. 243-250. - ISBN: 979-8-3503-2543-0. Proceedings of: 1st International Workshop on Verification & Validation of Dependable Cyber-Physical Systems, Porto, Portugal, 27 June 2023. - DOI: 10.1109/DSN-W58399.2023.00063

On CNF Conversion for Disjoint SAT Enumeration
Masina, Gabriele; Spallitta, Giuseppe; Sebastiani, Roberto in Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, p. 1501-1516. - (LEIBNIZ INTERNATIONAL PROCEEDINGS IN INFORMATICS). - ISBN: 978-3-95977-286-0. Proceedings of: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), Alghero, Italia, 4th-8th July 2023. - Publication URL . - DOI: 10.4230/lipics.sat.2023.15

Asynchronous Composition of Local Interface LTL Properties
Bombardelli, Alberto; Tonetta, Stefano in NASA Formal Methods 14th International Symposium, NFM 2022, GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND: SPRINGER INTERNATIONAL PUBLISHING AG, 2022, p. 508-526. - ISBN: 978-3-031-06772-3. Proceedings of: NFM22, Pasadena, CA, USA, May 24-27, 2022. - DOI: 10.1007/978-3-031-06773-0_27

SMT-based Weighted Model Integration with Structure Awareness
Spallitta, Giuseppe; Masina, Gabriele; Morettin, Paolo; Passerini, Andrea; Sebastiani, Roberto in Proceedings of UAI 2022, SL: SN, 2022. Proceedings of: UAI, Eindhoven, 1-5 August, 2022. - Publication URL

Verification of SMT Systems with Quantifiers
Cimatti, A.; Griggio, A.; Redondi, G. in International Symposium on Automated Technology for Verification and Analysis, Cham, Svizzera: Springer, 2022, p. 154-170. - (LECTURE NOTES IN COMPUTER SCIENCE). - ISBN: 978-3-031-19991-2. Proceedings of: ATVA, Virtual, 25-28 october, 2022. - Publication URL . - DOI: 10.1007/978-3-031-19992-9_10

NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
Amendola, Arturo; Becchi, Anna; Cavada, Roberto; Cimatti, Alessandro; Ferrando, Andrea; Pilati, Lorenzo; Scaglione, Giuseppe; Tacchella, Alberto; Zamboni, Marco in Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND: SPRINGER INTERNATIONAL PUBLISHING AG, 2022, p. 125-142. - (LECTURE NOTES IN ARTIFICIAL INTELLIGENCE). - ISBN: 978-3-030-99523-2. Proceedings of: TACAS, Munich, Germany, 2nd April-7th April 2022. - DOI: 10.1007/978-3-030-99524-9_7

Abstraction Modulo Stability for Reverse Engineering
Becchi, A; Cimatti, A in Computer Aided Verification - 34th International Conference, GEWERBESTRASSE 11, CHAM, CH-6330, SWITZERLAND: SPRINGER INTERNATIONAL PUBLISHING AG, 2022, p. 469-489. - (LECTURE NOTES IN ARTIFICIAL INTELLIGENCE). - ISBN: 978-3-031-13184-4. Proceedings of: CAV, Haifa, Israel, August 7-10, 2022. - DOI: 10.1007/978-3-031-13185-1_23

Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning
Cimatti, A.; Griggio, A.; Redondi, G. in Automated Deduction – CADE 28, Cham, Svizzera: Springer, 2021, p. 131-147. - (LECTURE NOTES IN COMPUTER SCIENCE). - ISBN: 978-3-030-79875-8. Proceedings of: 28th International Conference on Automated Deduction, CADE 28 2021, Online, 12-15 July, 2021. - Publication URL . - DOI: 10.1007/978-3-030-79876-5_8

PPLite: Zero-overhead encoding of NNC polyhedra
Becchi, A; Zaffanella, E in INFORMATION AND COMPUTATION, v. 275, (2020), p. 104620. - DOI: 10.1016/j.ic.2020.104620

A Model-Based Approach to the Design, Verification and Deployment of Railway Interlocking System
Amendola, Arturo; Becchi, Anna; Cavada, Roberto; Cimatti, Alessandro; Griggio, Alberto; Scaglione, Giuseppe; Susi, Angelo; Tacchella, Alberto; Tessi, Matteo in Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Cham, Switzerland: Springer, 2020, p. 240-254. - ISBN: 978-3-030-61466-9. Proceedings of: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020. - DOI: 10.1007/978-3-030-61467-6_16