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