Software Engineering and Formal Methods
Our goal is to develop languages, methods, techniques and tools to support the design and deployment of trustworthy and effective software systems.
Publications
19 publications for 7 currently enrolled students
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
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
Students
Becchi, Anna | anna.becchi [at] unitn.it | webpage | |
Bombardelli, Alberto | alberto.bombardell-1 [at] unitn.it | webpage | |
Goyal, Srajan Kumar | srajankumar.goyal [at] unitn.it | webpage | |
Kherrour, Aya | aya.kherrour [at] unitn.it | webpage | |
Masina, Gabriele | gabriele.masina [at] unitn.it | webpage | |
Redondi, Gianluca | gianluca.redondi [at] unitn.it | webpage | |
Spallitta, Giuseppe | giuseppe.spallitta [at] unitn.it | webpage |