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

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. McCormick, John W.; Chapin, Peter C.: Building high integrity applications with SPARK (2015)