Research Team Status

• Jonathan Aldrich, Professor, School of Computer Science
• Joshua Sunshine, Assistant Professor, School of Computer Science

We are also collaborating with Jenna DiVincenzo at Purdue University, who pioneered gradual verification in her thesis work with Jonathan and Joshua.

Project Goals

Following the research program outlined in our technical proposal, our primary current project goal is developing a Continuous Assurance system.  This system will support incremental progress in writing and evolving proofs about code by integrating static and dynamic verification in the context of continuous integration.

The basic Continuous Assurance system is a first step that makes it easier to evolve proofs by providing continuous feedback about the consistency and correctness of specifications and code.  It is also a foundation for later parts of the project, including a proof maintenance system that quickly restores static and dynamic verifiability after a change to code, and a proof repair system that helps developers make more comprehensive fixes to proofs that were broken by software evolution.  Together, we believe these systems will have a substantial effect on maintaining proofs over time.

Accomplishments

We have begun the design of an integrated development environment (IDE) supporting continuous assurance in support of the first project goal.  The IDE will enable developers to maintain constant consistency between their code and its specifications through both static and dynamic checking.  A key aspect of this approach is a proof debugger that helps developers understand the symbolic state of the verifier at every program point, allowing the developer to quickly understand and fix problems with their proofs.  We believe the debugger will significantly increase the usability of the continuous assurance, automatic proof repair, and proof generation tools in our continuous reasoning for gradual verification project.

While we have not reached any project milestones yet, the accomplishments represent progress that puts us on track to meet our first milestone, scheduled for a year after the project started (i.e. end of January 2025).

Impact / contributions of research - N/A as we are only 3 months into the project.

Publications and presentations

N/A as we are only 3 months into the project.