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.
Program Analysis in the Face of Uncertainty
