Managing the Proof Context in SPARK

SPARK performs verification of Ada programs in an autoactive style: the verification is done by automated solvers, but users need to write annotations in the source code - in general contracts - for the proof to succeed. For auto-active verification of programs to scale, managing the size of the proof context given to automated solvers is key. This paper will describe the various mechanisms and heuristics used in SPARK to reduce the size of the proof context. They range from completely automated to manual, taking full advantage of the auto-active verification style.