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. During my PhD, I’ve spent some time at FBK, at the Czech Academy of Sciences, and at SRI International. 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, accepted at CADE’25 [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

• Formal Methods for Blockchains - FMBC’25, Hamilton, Canada, May 2025
• 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