Formal Methods

Logical errors in computer hardware and software can have significant economic and societal impact, while errors in the embedded systems that are increasingly used in safety-critical applications like “drive-by-wire” and implantable medical devices, can lead to loss of human life. Our formal methods group aims to help hardware and software engineers build more reliable systems through model checking — a technique that relies on building a finite model of a system and checking that a desired property holds in that model. The technical challenge in model checking is in devising algorithms and data structures that allow us to handle large search spaces. Model checking is fast, automatic, and supports partial specifications. Above all, it produces counterexamples, which usually represent subtle errors in design and can aid in debugging.

At Carnegie Mellon we promote lightweight formal methods. Rather than try to specify all properties of an entire system and attempt to do a complete proof of correctness, we advocate specifying critical properties of a critical part of a system and focus on finding errors. “Spec ’n Check” is our mantra. Our techniques scale beyond what people can do by hand and avoid fallibility of human reasoning.

Faculty working in this area:

Lastsort descending First Title Email
Aldrich Jonathan Associate Professor; Director, Software Engineering Ph.D. Program aldrich@cs.cmu.edu
Brookes Stephen Professor brookes@cs.cmu.edu
Brumley David Affiliated Faculty dbrumley@cs.cmu.edu
Bryant Randy University Professor bryant@cs.cmu.edu
Clarke Edmund Faculty Emeritus ec10@andrew.cmu.edu
Datta Anupam Associate Professor, CSD, ECE danupam@andrew.cmu.edu
Fredrikson Matthew Assistant Professor mfredrik@andrew.cmu.edu
Garlan David Co-Director, Software Engineering Masters Programs; Professor garlan@cs.cmu.edu
Harper Robert Professor rwh@cs.cmu.edu
Hoffmann Jan Assistant Professor janh@andrew.cmu.edu
Pfenning Frank Department Head; Professor fp@cs.cmu.edu
Platzer André Associate Professor aplatzer@cs.cmu.edu
Simmons Reid Research Profesor; Associate Director of Education, Robotics Institute; Ph.D. Chair, Robotics Institute reids@cs.cmu.edu
Subscribe to Formal Methods