Current Research
- Software Verification (e.g., model checking, symbolic summarization, program termination)
- Incremental Model Checking (e.g., abstraction-based analysis, function summarization, interpolation-based upgrade checking)
- Automated Invariant Discovery for Array-based Systems (e.g., SAFARI approach)
- Formal Verification via Boolean and Theory Reasoning (SMT) (e.g., SAT/SMT-based model checking)
- Formal Verification via Interpolation (e.g., Craig interpolation for symbolic model checking, proof transformation)
Description of
funded projects can be found
here.