Image courtesy BAE Systems
 
Current formal methods tools, a type of software verification, provide high levels of assurance through mathematical proofs that certain properties hold, but can be time-consuming and difficult to learn and use. These proofs also need to be re-written at every code or specification change, which fails to scale.

 
The goal of PROVERS is to make formal methods accessible to non-experts (e.g. traditional software developers and systems engineers) while minimising the impact on their existing processes and performance.
 
“Engineering practices for software-reliant systems continuously evolve, and so too must the assurance techniques that confirm systems’ correctness and security,” said Daniel Mitchell, technical manager at BAE Systems’ FAST Labs research and development organisation. “With PROVERS, proof engineering will create higher levels of assurance – helping critical Department of Defense software systems remain free of certain defects and vulnerabilities.”
 
Under the terms of the contract, BAE Systems will provide a Department of Defense (DoD) - relevant system to demonstrate how formal methods tools can integrate into the development and certification process and provide assurance of correctness. The company’s software engineers will also provide feedback to developers on how to ensure formal methods tools are applicable to DoD systems and how to make those tools accessible to them.
 
Work on this programme will take place at BAE Systems’ facilities in Merrimack, New Hampshire; Burlington, Massachusetts and Arlington, Virginia.