Impactful Research and Tooling for Program Correctness

In 2020, poor-quality software systems led to financial losses of approximately USD 2.08 trillion in the U.S. alone.19 Formal methods, such as bounded model checking (BMC), help to improve software quality, but they often fail to scale to the size and complexity of software.