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.
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)	We are developing a new open-source SMT-solver which allows us to experiment with all our ideas on new SMT theories.