Enrico Lipparini
I am a Postdoctoral Researcher in Computer Science at the University of Cagliari working in Massimo Bartoletti’s group. I received my PhD from the University of Genoa in 2024, under the supervision of Stefan Ratschan and Alessandro Armando. I graduated in Mathematics from the University of Milan in 2020, under the supervision of Silvio Ghilardi.
Main interests:
- Formal Verification
- Satisfiability Modulo Theory (SMT)
- Smart Contracts
Publications
-
“Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search”, Enrico Lipparini, Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand, (preprint), 2025 [pdf]
-
“Formal verification in Solidity and Move: insights from a comparative analysis”, Massimo Bartoletti, Silvia Crafa, Enrico Lipparini, in FMBC’25 [pdf]
-
“Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem”, Enrico Lipparini, Stefan Ratschan, in Journal of Automated Reasoning, 2024
-
“Solvent: Liquidity Verification of Smart Contracts”, Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini, Vadim Malvone, in iFM’24 [pdf]
-
“Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem”, Enrico Lipparini and Stefan Ratschan, in NFM’23 [pdf]
-
“Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test”, Alessandro Cimatti, Alberto Griggio, Enrico Lipparini, Roberto Sebastiani, in ATVA’22 [pdf, slides, video]
Theses
-
PhD: “Satisfiability modulo Nonlinear Arithmetic and Transcendental Functions via Numerical and Topological methods”, (supervisors: Stefan Ratschan, Alessandro Armando), 2024 [pdf]
-
MSc: “Decision Techniques for Parameterized Verification: the case of Token-Passing Rings” (supervisor: Silvio Ghilardi), 2020 [pdf]
Academic Service
- PC member of ECAI’25
- PC member of FMBC’25
- PC member of IWBOSE’25
- External Reviewer / sub-Reviewer for: Acta Informatica, COORDINATION’25, CAAW’25, FC’25, FMCAD’24, SMT’24, CAV’22, IJCAR’22, SEFM’22, TACAS’21
Talks
- Integrated Formal Methods - iFM’24, Manchester, UK, November 2024
- Secure Software from First Principles Workshop - SWOPS’24, Lucca, Italy, June 2024
- Alpine Verification Meeting - AVM’23, Prague, Czech Republic, September 2023
- SMT Workshop - SMT’23, Rome, Italy, July 2023
- NASA Formal Methods Symposium - NFM’23, Houston, USA, May 2023
- Automated Technology for Verification and Analysis - ATVA’22, Beijing, China (online), October 2022
- Alpine Verification Meeting - AVM’22, Frauenchiemsee, Germany, September 2022
- New Perspectives in Symbolic Computation and Satisfiability Checking - Dagsthul Seminar 22072, Germany, February 2022