bionic (1) victor.1.gz

NAME

       victor - attempts to discharge verification conditions using SMT solvers

SYNOPSIS

       victor [UNIT]

DESCRIPTION

       The  victor  command  is  a wrapper around ViCToR (vct) which simplifies its use. ViCToR translates SPARK
       verification conditions into SMTlib and feeds them to an SMT  solver.  SPARK  ships  with  one  such  SMT
       solver, alt-ergo, but it is possible to use others solvers such as cvc3.

       The  intended  use  of  victor  is  to discharge true VCs left over by the Simplifier and not replace the
       Simplifier. Please also note that ViCToR is considered to be an experimental feature at the moment.

       This manual page only summarises the victor command-line flags, please refer to  the  full  VictorWrapper
       manual for further information.

OPTIONS

       These  options  do not quite follow the usual GNU command line syntax as options start with a single dash
       instead of the usual two.

       -h, -help
              Shows command-line help.

       -t=SECONDS
              Time-out the SMT solver after this many seconds (by default 5) using ulimit. To  disable  time-out
              specify 0.

       -m=MEGABYTES
              Limit the SMT solver to this many MiB of virtual memory (by default no limit) using ulimit.

       -v     Ignore  the presence of any siv files and process vcg files only. By default, given a UNIT such as
              foo, victor will first attempt to process foo.siv and then fall back to foo.vcg.

       -plain Plain mode — supress timings and versions.

       -solver=SOLVER
              Specifies an alternative SMT solver. By default we use alt-ergo. Can be  one  of  alt-ergo,  cvc3,
              yices or z3. The alt-ergo solver is distributed with SPARK. The cvc3 solver is part of Debian. The
              yices and z3 solvers are proprietary.

SEE ALSO

       spark(1), sparksimp(1), spadesimp(1), zombiescope(1), pogs(1)

       sparkformat(1), sparkmake(1)

       cvc3(1)

AUTHOR

       This manual page was written  by  Florian  Schanda  <florian.schanda@altran-praxis.com>  for  the  Debian
       GNU/Linux  system  (but  may  be used by others). Permission is granted to copy, distribute and/or modify
       this document under the terms of the GNU Free Documentation License, Version 1.3  or  any  later  version
       published  by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts and no Back-
       Cover Texts.

                                                  22 March 2011                                        victor(1)