Software Engineering and Formal Methods | Doctoral Program - Information Engineering and Computer Science

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, Annaanna.becchi [at] unitn.itwebpage
Bombardelli, Albertoalberto.bombardell-1 [at] unitn.itwebpage
Goyal, Srajan Kumarsrajankumar.goyal [at] unitn.itwebpage
Kherrour, Ayaaya.kherrour [at] unitn.itwebpage
Masina, Gabrielegabriele.masina [at] unitn.itwebpage
Redondi, Gianlucagianluca.redondi [at] unitn.itwebpage
Spallitta, Giuseppegiuseppe.spallitta [at] unitn.itwebpage