Research interests


We focus on the following aspects of automated formal verification.

Current projects carried out by our Lab:

Model Checkers


Formal Verification of Smart Contracts


Smart contracts are programs written in Turing complete languages that can be deployed to specific blockchain platforms. Due to the nature of their application, they can hold and manipulate significant monetary assets, which marks them as tentative targets for attackers. In addition, their execution in blockchain platforms leads to financial costs that need to be managed properly, or significant monetary loss is possible. In this project we investigate the application of formal verification in this context, tackling both safety issues, as well as execution costs, i.e. contracts' gas consumption.


Harnessing Parallel Computing for Model Checking


Veirifying complex software can be extremely expensive.  In this project we address the challenges of software verification with an extensive parallel model checking framework able to scale both to multi-core, grid and cloud computing and address key aspects of model checking, including underlying SMT solver, model-checking algorithms and related technologies such as interpolation.


Automated Invariant Discovery for Array-based Systems


The project goal is to study, design and develop new technologies and frameworks for efficient invariant discovering by means of model checking. Innovative abstraction/refinement techniques will be investigated and integrated in a tool, SAFARI, that will be use to prove the effectiveness of our approaches.


Bounded Incremental Model Checking


This project is aimed to develop new techniques for checking the software upgrades based on successful verification of the source program and reusing the invested effort. It is currently based on a bounded model checker with interpolation-based function summaries, which can be applied to improve efficiency of model checking of the single source program, as well as its upgraded version.

Decision Procedures


Unbounded Property Directed Equivalence and Simulation Synthesis


This project targets establishing a so called Property Directed Equivalence. We build the first technique to effectively exploit both, the reusable specification of software (by means of safe inductive invariants) and the relational specification of software (by means of simulation relations), to incrementally verify sequences of program versions with non-trivial loop structures and non-trivial transformations. Our approach succeeds in many cases when the absolute equivalence between programs cannot be proven.


Formal Verification via Boolean and Theory Reasoning (SMT)


The project focuses on SMT-solving and its applications. We are investigating new efficient decision procedures for SMT, interpolation techniques for several theories of interest and their combinations. Research and experimentation are carried out with the help of OpenSMT, our state-of-the-art open-source SMT-Solver.

Completed projects:


Detection of Security Flaws and Vulnerabilities by Guided Model Checking


This project tailors state-space reduction algorithms to the code security domain and focuses on the development of specialized model checking algorithms for detecting security vulnerabilities. It currently includes new program summarization and program termination techniques developed in our Lab.


The Synergy of Precise and Fast Abstractions for Program Verification


This project proposes a new abstraction refinement technique that combines slow and precise predicate abstraction techniques with fast and imprecise ones. The new synergy technique outperforms both precise and overapproximated methods taken in isolation.


Automated Verification of Security Policies in Mobile Code


This project defines a model checking-based approach for verification of mobile programs against security policies. As compared to all previous approaches, it verifies mobile programs at source level.