publications

2024

1. Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)

   Raphaël Monat, Marco Milanese, Francesco Parolini, and 3 more authors

   In Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III , 2024

   Bib PDF

   @inproceedings{monat_mopsa_2024,
     author = {Monat, Rapha{\"{e}}l and Milanese, Marco and Parolini, Francesco and Boillot, J{\'{e}}r{\^{o}}me and Ouadjaout, Abdelraouf and Min{\'{e}}, Antoine},
     editor = {Finkbeiner, Bernd and Kov{\'{a}}cs, Laura},
     title = {Mopsa-C: Improved Verification for {C} Programs, Simple Validation
                       of Correctness Witnesses (Competition Contribution)},
     booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
                       - 30th International Conference, {TACAS} 2024, Held as Part of the
                       European Joint Conferences on Theory and Practice of Software, {ETAPS}
                       2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings,
                       Part {III}},
     series = {Lecture Notes in Computer Science},
     volume = {14572},
     pages = {387--392},
     publisher = {Springer},
     year = {2024},
     url = {https://doi.org/10.1007/978-3-031-57256-2\_26},
     doi = {10.1007/978-3-031-57256-2\_26},
     timestamp = {Fri, 17 May 2024 21:42:14 +0200},
   }

2. Generation of Violation Witnesses by Under-Approximating Abstract Interpretation

   Marco Milanese, and Antoine Miné

   In Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I , 2024

   Bib PDF

   @inproceedings{milanese_generation_2024,
     author = {Milanese, Marco and Min{\'{e}}, Antoine},
     editor = {Dimitrova, Rayna and Lahav, Ori and Wolff, Sebastian},
     title = {Generation of Violation Witnesses by Under-Approximating Abstract
                       Interpretation},
     booktitle = {Verification, Model Checking, and Abstract Interpretation - 25th International
                       Conference, {VMCAI} 2024, London, United Kingdom, January 15-16, 2024,
                       Proceedings, Part {I}},
     series = {Lecture Notes in Computer Science},
     volume = {14499},
     pages = {50--73},
     publisher = {Springer},
     year = {2024},
     url = {https://doi.org/10.1007/978-3-031-50524-9\_3},
     doi = {10.1007/978-3-031-50524-9\_3},
     timestamp = {Fri, 26 Jan 2024 07:55:26 +0100},
   }

2022

1. Local Completeness Logic on Kleene Algebra with Tests

   Marco Milanese, and Francesco Ranzato

   In Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5-7, 2022, Proceedings , 2022

   Bib PDF

   @inproceedings{local_milanese_2022,
     author = {Milanese, Marco and Ranzato, Francesco},
     editor = {Singh, Gagandeep and Urban, Caterina},
     title = {Local Completeness Logic on Kleene Algebra with Tests},
     booktitle = {Static Analysis - 29th International Symposium, {SAS} 2022, Auckland,
                       New Zealand, December 5-7, 2022, Proceedings},
     series = {Lecture Notes in Computer Science},
     volume = {13790},
     pages = {350--371},
     publisher = {Springer},
     year = {2022},
     url = {https://doi.org/10.1007/978-3-031-22308-2\_16},
     doi = {10.1007/978-3-031-22308-2\_16},
     timestamp = {Sun, 25 Dec 2022 14:02:21 +0100},
   }