Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS)
Abstract
The Pipelined Reasoning of Verifiers Enabling Robust Systems (PROVERS) program aims to advance the capability, scope, and usability of scalable mathematically based technologies, tools, and practices to achieve continuous reasoning about complex systems that can support software development pipelines. These mathematically based techniques, or formal methods, enable rigorous modeling, reasoning, and proving diverse properties of software code or design models, for example the absence of a specific type of defect or security vulnerability. PROVERS will integrate formal methods into a modern incremental and iterative development process by running tools at each code commit and delivering results to developers when they can most effectively remediate discovered issues. To achieve this, PROVERS will focus on creating and sustaining a body of evidence that can co-evolve with the system under change to support continuous assessment and ensure that the system remains free of identified categories of defects and security vulnerabilities through its lifetime. Key PROVERS objectives include enabling proof maintenance and repair capabilities at a cost that is proportionate to code change; integration of formal methods with code, properties, and proofs in a single workflow that reduces human involvement; providing improved explanations to facilitate proof repair; and automating formal methods-based software analysis to support software developers that are not formal methods experts. PROVERS technologies will facilitate the agile development and continuous improvement of mission-critical software systems that meet the high security and quality standards required by the DoD.
Document Details
- Document Type
- Accomplishment
- Publication Date
- Oct 01, 2023
- Source ID
- ba25a1ddf38aec12e890712e980aa167