Abstract
SPARK is an open source program proof technology based on data flow analysis and deductive verification for programs written in the Ada programming language. SPARK is co-developed by AdaCore, Altran and Inria, and marketed by AdaCore in various critical fields (avionics, military, space, rail, automotive, medical).
In this seminar, Yannick Moy presented the choices that have been made for SPARK's specification language and associated proof tool, the difficulties of application in practice, and how the auto-active proof approach addresses them. He discussed recent improvements to the specification language and tool to handle partially initialized data and pointers without aliasing.
