Research interests

We focus on the following aspects of automated formal verification.

Projects carried out by our Lab:


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.
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.
Formal verification of software changes and upgrades	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.
The Synergy of Precise and Fast Abstractions for Program Veriﬁcation	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.
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; we are also building a framework for resolution proofs transformation and reduction. Research and experimentation are carried out with the help of OpenSMT, our state-of-the-art open-source SMT-Solver.