Victor: A SPARK Verification Condition Translator and Prover Driver

Overview

SPARK is an Ada subset which adds in an annotation language for expressing desired program properties.

Victor translates verification conditions (VCs) generated from SPARK programs into formats accepted by popular theorem provers. It also can automatically run these provers on the translated VCs.

VCs are logical statements that, if proven, formally guarantee the programs they are generated from satisfy certain correctness conditions. For example, the guarantees can be for the absence of run-time errors such as overflows and array bounds violations. Guarantees can also concern the correctness of program annotations.

Formats supported by Victor include

The SPARK Toolset

Formal verification of SPARK programs is supported by the SPARK toolset from Altran Praxis and AdaCore. Altran Praxis originally developed the toolset. AdaCore distribute the toolset, provide customer support services, and incorporate the toolset into their integrated development environment for Ada (the GNAT Programming Studio or GPS).

The SPARK toolset includes tools for both generating and proving VCs:

Victor augments the capabilities of the SPARK toolset provers by providing access to alternate proof technologies. Both the toolset and GPS provide options for running Victor in conjunction with the Alt-Ergo SMT solver. Alternatively, in combination with any appropriate prover, Victor can be run as a stand-alone tool on the VCs produced by the Examiner and on simplified VCs that the Simplifier is unable to prove.

Links:

Documentation

Source Code and Downloads

Victor is released under the GNU GPL v3 license.

Victor currently only compiles and runs on Linux systems. Altran Praxis and AdaCore are working on a Windows port.

Victor is hosted as the vct project on Google Code. Visit the Downloads tab for the latest release and the Source tab to see the current development code.

The current release is 0.9.1 (15th December 2010).

To install a release tarball, unpack it with a command such as

  tar xzf vct-0.9.0.tgz
and consult the file README.txt in the main directory for further instructions.

Mail List

A mail list vct-users@googlegroups.com has been set up for Victor users. Visit the list's home page to view postings or request to be added to the list. Use the list for asking questions about use, requesting features and reporting bugs. Announcements of future releases will be posted to this list.

Future developments

Here are some ideas for future next steps. Currently there are no definite plans for any of these to happen. If you are a Victor user and might be interested in any of these, please get in touch. Or, if you would like to take on a project to add any of these features yourself, please get in touch too.
Last modified: Fri 1 Jun 2012