GNATProve is used for formal verification of Ada programs and is being developed as part of the Hi-Lite project. It can prove that subprograms respect their contracts, expressed as preconditions and postconditions in the syntax of Ada 2012. The tool automatically discovers the subset of subprograms which can be formally analyzed. We provide binary distributions for x86 linux, x86 windows and x86-64 bit linux. More details can be found at http://www.open-do.org/projects/hi-lite/gnatprove/
Press Release
Oct 16 '12
