Research areas

Our innovative approach to formal verification combines model checking and related logic-based reasoning. In particular, our solutions focus on the integrated development of efficient SAT/SMT solvers.

The following are the current projects carried out by our Lab:

Software Model Checking
Bounded Incremental Model Checking This project is aimed to develop new techniques for verifying the software in C based on successful verification of the source program and reusing the invested effort in consecutive verification runs. It is currently based on a bounded model checker with interpolation-based function summaries, which can be applied to improve the efficiency of model checking of the single-source program with multiple properties (see FunFrog and HiFrog), as well as model checking of different revisions of a program w.r.t a fixed property (see eVolCheck and UpProver).

Formal Verification of Smart Contracts

Smart contracts are programs that can be deployed on specific blockchain platforms. Due to the nature of their application, they often hold and manipulate significant financial assets, which marks them as tentative targets for attackers. In addition, their execution in blockchain platforms leads to costs that need to be managed properly, otherwise users can incur significant financial loss. In this project we investigate the application of formal verification in tackling both contracts' safety and execution costs.

Certified Execution of Verification Tools

 Verification tools often rely on back-end reasoning engines to achieve their results. Despite being used in safety-critical contexts, reasoning engines are known to have bugs, which may be a source of unsoundness in verification. In this project we investigate how results from different reasoning engines can be validated and how they can provide additional guarantees for verification tools.

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.
Solving Constrained Horn Clauses for Formal Verification

Constrained Horn clauses have emerged recently as an intermediate layer in the process of software verification. Verification tasks from many different domains can be encoded to the common language of constrained Horn clauses (CHC) and a single CHC solver can be re-used for the actual solving. This project aims to develop an efficient and reliable CHC solver to facilitate the development and deployment of verification frameworks.

Automated Invariant Discovery for Array-based Systems

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

Constrained Horn clauses

Constrained Horn clauses have emerged recently as an intermediate layer in the process of software verification. Verification tasks from many different domains can be encoded to the common language of constrained Horn clauses (CHC) and a single CHC solver can be re-used for the actual solving. This project aims to develop an efficient and reliable CHC solver to facilitate the development and deployment of verification frameworks. Check out our CHC solver Golem

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.

Harnessing Parallel Computing for Model Checking

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

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 the source level.