Part of the Hi-Lite project, GNATprove is a formal verification tool for Ada, based on the GNAT compiler, Why3 platform and Alt-Ergo prover. 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. GNATprove is currently available for x86 linux, x86 windows and x86-64 linux.
Keywords for this software
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.