Writing Notes

Formal Methods

Logical errors in computer hardware and software can have significant economic and societal impact, threatening safety and security.

Our formal methods group aims to help hardware and software engineers build systems that are correct, reliable and secure.  

We do this by designing and employing techniques that provide rigorous guarantees about the properties of hardware and software; e.g., by proving that code will give the correct answer for all possible inputs.  We are interested in approaches based on programming languages, type systems, formal verification, and automated reasoning tools (e.g., SAT and SMT solvers).  

We are motivated both by abstract mathematical problems and by concrete systems used in practice.  Results from our group have resolved decades-old mathematical conjectures, as well as been deployed to improve the correctness and security of software systems used by hundreds of millions of people.

Events

CyLab Seminar

Program Analysis in the Face of Uncertainty

Researchers Working in this Area

Last First Professional Title
Aldrich Jonathan Professor, Affiliated Faculty
Brookes Stephen Professor Emeritus
Brumley David Professor of ECE, Affiliated Faculty
Fredrikson Matt Associate Professor
Garlan David Professor
Harper Robert Professor
Heule Marijn Associate Professor
Hoffmann Jan Associate Professor
Parno Bryan Professor
Pfenning Frank Professor
Wing Jeannette Adjunct Faculty
Subscribe to Formal Methods