- Formal Verification of Industrial Critical Systems
- Symbolic Model Checking (BDD-based, SAT-based, SMT-based, Bounded Model Checking)
- Software model checking of sequential and concurrent code
- Planning in Nondeterministic Domains via Symbolic Model Checking
- Formal requirements analysis
- Decision procedures and their application to formal verification
![](http://es.fbk.eu/people/roveri/home/images/research.png)
(thanks to world cloud)