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 standard SMT-LIB language supported by
many SMT solvers. Victor has been specifically tested with the
SMT-LIB interfaces of the SMT solvers
- API calls for the CVC3 and Yices SMT solvers.
- Theory files for the
Isabelle/HOL
interactive theorem prover.
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:
- The Examiner generates the VC files that Victor reads in.
- The Simplifier is an automatic VC prover
- The Checker is an interactive VC prover
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.
- Improvement of support for proving VCs using interactive
theorem provers
The current Victor has some preliminary code for interfacing to
Isabelle/HOL. Fabian Immler at TU M&um;nchen developed this further
in 2010 and Secunet took
some interest in this interface. (Secunet since have developed
their own SPARK FDL Isabelle/HOL interface.)
Interfaces to other theorem provers such as PVS and HOL Light would
be interesting to explore.
Continued work on interfaces almost-certainly ought to exploit the
incremental prover driver in order to write out a single prover
input file for each SPARK unit.
- An API interface for Z3. This could offer improved performance
and increased functionality.
- A native-language Alt-Ergo interface.
This could offer improved performance and
increased functionality, especially as the Alt-Ergo team currently
appear to be emphasising support for its native input language over
either SMTLIB 1.2 or SMTLIB 2.0.
- Exploitation of Z3 SMTLIB 2 extensions for arrays and
records. Again, a benefit could be improved performance.
- Exploitation of the bit-vector handling capabilities of SMT
solvers.
As a pre-processing step, this would involve recovering
finite range information for integer-typed constants, functions and
variables.
- Exploration of counter-example generation. With the usual high
number of quantified hypotheses and rules, SMT solvers virtually
always report an unknown result rather than a sat
result when proof fails.
How could SMT solvers be persuaded to still return some tentative
counter-example information, perhaps with some indication of which
quantified assumptions were not fully examined and potentially could
still refute the counter-example?
The riposte
project has been exploring counter-example generation using answer-set
programming. It would interesting to compare counter-examples
produced by these two alternative methods.
Last modified: Fri 1 Jun 2012