Research interests

We focus on the following aspects of automated formal verification.

Current projects carried out by our Lab:

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.

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.

Formal Verification via Boolean Reasoning and Interpolation

The project focuses on SAT-solving and Craig interpolation in the resolution system. We are studying the impact of features of interpolants such as logical strength and size on verification; interpolation is examined in combination with techniques for manipulating the resolution refutations from which the interpolants are computed. Research and experimentation are carried out with the help of PeRIPLO, our state-of-the-art open-source SAT-Solver, which implements a framework for interpolation and proof manipulation.


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.