| title | Cooperative Program Verification |
|---|---|
| image | /images/projects/ProgramVerification.png |
| date | 2019-05-31 |
| team | Mitchell J. Gerrard, Will Leeson, and Matthew B. Dwyer |
| label | Foundational |
| sponsor | 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 |
| artifactlink | https://bitbucket.org/mgerrard/alpaca |
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 trade off 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.