~ Francesco Parolini

I am a PhD student in Computer Science at the Sorbonne University (Paris) under the supervision of Professor Antoine Miné, within the ERC MOPSA project. From October 2022 to March 2023 I have been an applied scientist intern working in the Amazon Prime Video Automated Reasoning group. Previously, I obtained a BSc and an MSc in Computer Science at University of Padua (Italy). For my Master's Thesis I worked on the language inclusion problem for ω-regular languages.

My research interests include security and automated formal methods, in particular by abstract interpretation.

💼 From April 2024, I will join Lacework in London as a software engineer.
🥇Mopsa, the static analyzer developed within my research team, won the gold medal by a long shot in the SoftwareSystems category of SV-COMP.

Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution).
Raphaël Monat, Marco Milanese, Francesco Parolini, Jérôme Boillot, Abdelraouf Ouadjaout, Antoine Miné. In TACAS, 2024.
PDF SV-COMP results
Sound Abstract Nonexploitability Analysis.
Francesco Parolini, Antoine Miné. In VMCAI, 2024.
Article PDF (HAL) BibTeX Code
Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks (Extended Version).
Francesco Parolini, Antoine Miné. In Science of Computer Programming, 2023.
Article PDF (HAL) BibTeX Code
Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks.
Francesco Parolini, Antoine Miné. In TASE, 2022.
Article PDF (HAL) BibTeX Code
Inclusion Testing of Büchi Automata Based on Well-Quasiorders.
Kyveli Doveri, Pierre Ganty, Francesco Parolini, Francesco Ranzato. In CONCUR, 2021.
PDF BibTeX Code Talk
Simulation-based Inclusion Checking Algorithms for ω-Languages.
Master's Thesis, 2020.
PDF Slides

Mopsa: framework to write static analyses by abstract interpretation.
rat: Regular Expression Denial of Service (ReDoS) attacks static analyzer.
bait: (Büchi Automata Inclusion Tester) a ω-regular language inclusion checker. It relies on abstract interpretation theory, while being sound and complete.
pilisp: a garbage collected interpreter written in C for a dialect of Lisp inspired to Common Lisp. The main feature is that it supports homoiconicity (as Lisp 1.5). It also has a bytecode compiler and bytecode interpreter which make the interpreter faster than CLISP.

Email	[surname].[name].1[at]gmail.com
Github	github.com/parof
Phone	+33 1 44 27 88 16
Team	APR
Location	Campus Pierre et Marie Curie, Sorbonne Université
	Boîte courrier 169 Couloir 25-26, Étage 3, Bureau 303
	4 place Jussieu
	75252 PARIS CEDEX 05
	France