Model Checking-based Software Verification
The goal of this research is to improve the overall precision and scalability of software model checking algorithms [1].
To attack this problem, we leverage the advantages of a variety of techniques from dynamic analysis (e.g., testing and symbolic execution) to static analysis (e.g., model checking and predicate abstraction). For example, in a recent work [2], we used symbolic execution to guide the building of finite abstract models of the program in question in order to facilitate verification.
We are currently working on exploiting the power of Craig Interpolation to build modular software model checking algorithms.
[1] Ranjit Jhala, Rupak Majumdar, Software Model Checking, ACM Computing Surveys, Oct 2009
[2] Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik, Abstract Analysis of Symbolic Executions, Computer Aided Verification (CAV), 2010
Other related projects: -Yogi Project (MSR)