Foundational Verification and Validation

Our group is currently leading work in the following areas:

Cooperative Program Verification

Cooperative Program Verification

Program verification is a powerful tool used to prove that safety critical software will not fail due to an unforeseen bug. However, its power comes with the tradeoff that it can be prohibitively expensive to run. In our group, we are developing ways to both lessen the expense of verification and enhance its precision. We are developing tools that leverage the power of existing verifiers to work in tandem and produce a more precise answer at a lesser expense. We are also creating tools that will divide a program in such a way that verification can be done in parallel and is simplified by reducing the state space tools have to reason about.

Team Members: Mitchell J. Gerrard, William Leeson, and Matthew B. Dwyer
Sponsors: This effort is supported by NSF Awards #1617916 and #1901769, the U.S. Army Research Office #W911NF-19-1-0054, as well as by the DARPA ARCOS program under contract #FA8750-20-C-0507