Model checking is a collection of automated formal reasoning techniques for analyzing and verifying computing systems. Our group conducts research on both high-performance implementation of model checking, and on complexity-theoretic analysis of model checking algorithms. Topics include: 

• SAT/QBF encodings for automated planning and 2-player games
• Symbolic model checking algorithms, using binary decisions or polyhedra
• High-performance model checking algorithms (multicore, external memory)
• Stateless model checking of concurrent systems 

Effective model checking techniques aim to aid system design, development and verification, in order to support a digital infrastructure that is more reliable and secure. Owing to their automated nature, these techniques require little expertise from their users, which is a key feature for widespread adoption and use.