Computer-aided verification of software and hardware – Model checking
Compositional model checking
Abstraction, refinement and counterexamples (CEGAR)
Temporal logics
Equivalences and preorders
SAT-based model checking
Automata on infinite objects
Finding security vulnerabilities with formal methods
Program repair
Program differencing
Distributed Model checking
Static analysis and model checking
Coverage and vacuity
Games for model checking
Symbolic Trajectory Evaluation (STE)
Symmetry