Pushing the Boundary of Mostly Automatic Program Proof
Static Analysis Lead, AdaCore
With the large-scale verification of complex programs like compilers and microkernels, program proof has realised the grand challenge of creating a “verifying compiler” proposed by Sir Tony Hoare in 2003. Still, the effort and expertise required for developing the program and its proof to feed to the “verifying compiler” will exceed the V&V budget of most projects. Another approach gaining traction is to automate the proof as much as possible. More specifically, by tailoring the proof tool to the strengths of a target programming language, leveraging an array of automatic provers, and limiting the ambition of proof to those properties for which proof can be mostly automated. This is the approach we are following in SPARK. In this talk, we will survey what properties can be “mostly” proved automatically, and what this means in terms of effort and expertise.
About Yannick Moy
Yannick Moy is Static Analysis Lead at AdaCore. Yannick leads the development of SPARK, a software source code analyser aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analysers for PolySpace (now The MathWorks) and at Université Paris-Sud.