Francesco Parolini

Static Analysis Software Engineer

About

I am a compiler engineer at Certora in London. Previously, I worked as a static analysis software engineer at Lacework. I hold a PhD in Computer Science from Sorbonne University (Paris), completed under the supervision of Professor Antoine Miné, as part of 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. 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.

News

  • 💼 In August 2024 I joined Certora in London as a compiler engineer.
  • 🎓 On the 26th of June 2024 I defended my PhD thesis: I am now a docteur en informatique de Sorbonne Université!
  • 🥇Mopsa, the static analyzer developed within my research team, won the gold medal by a long shot in the SoftwareSystems category of SV-COMP.

Research

  • Static Analysis for Security Properties of Software by Abstract Interpretation.
    PhD Thesis, 2024.
    PDF Slides
  • 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.
    Article PDF BibTeX SV-COMP results
  • Sound Abstract Nonexploitability Analysis.
    Francesco Parolini, Antoine Miné. In VMCAI, 2024.
    Article PDF 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 BibTeX Code
  • Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks.
    Francesco Parolini, Antoine Miné. In TASE, 2022.
    Article PDF BibTeX Code
  • Inclusion Testing of Büchi Automata Based on Well-Quasiorders.
    Kyveli Doveri, Pierre Ganty, Francesco Parolini, Francesco Ranzato. In CONCUR, 2021.
    Article PDF BibTeX Code Talk
  • Simulation-based Inclusion Checking Algorithms for ω-Languages.
    Master's Thesis, 2020.
    PDF Slides

Software

  • 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.

Contact

Email [surname].[name].1[at]gmail.com
Github phreppo
LinkedIn francesco-parolini

Service

  • I am a member of the CAV 2024 Artifact Evaluation Committee.
  • I was chair for the session "Abstract Interpretation" at CSV 2023
  • I am a member of the SAS 2023 Artifact Evaluation Committee.
  • I am a student volunteer at ETAPS 2023.
  • I am a member of the CAV 2023 Artifact Evaluation Committee.
  • I am a member of the SAS 2022 Artifact Evaluation Committee.
  • I am a member of the CAV 2022 Artifact Evaluation Committee.
  • I am a member of the SAS 2021 Artifact Evaluation Committee.

Return ⊤