NAME

       checker - SPARK Proof Checker

SYNOPSIS

       checker [OPTIONS] [FILE]

DESCRIPTION

       The  SPARK  Proof  Checker  can  be  used  to  discharge verification conditions produced by the Examiner
       (*.vcg), possibly simplified by the Simplifier (*.siv).  This command is usually used  when  verification
       conditions cannot be discharged automatically by the Simplifier.

       By  default  checker  runs in interactive mode.  It accepts commands from user and writes them into a cmd
       file (or other file specified by -command_log option).  This file can be used later  to  run  checker  in
       batch mode (using option -execute).  Additionally, proof log is written into a plg file.

OPTIONS

       A summary of options is included below.  All options may be abbreviated to the shortest unique prefix.

       -help  Show summary of options.

       -version
              Display version information.

       -plain Adopt a plain output style (e.g. no dates or version numbers).

       -overwrite_warning
              Confirmation needed to overwrite command or proof log files.

       -command_log=LOG_FILE
              Specify file name for the command log file.

       -proof_log=PLG_FILE
              Specify file name for the proof log file.

       -execute=LOG_FILE
              Execute a previously generated command log file.

       -resume
              Resume a previously saved session.

FILES

       /usr/share/spark/checker/rules/*
              Checker rules database.

SEE ALSO

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

AUTHOR

       This manual page was written by Eugeniy Meshcheryakov <eugen@debian.org>, for the Debian project (and may
       be used by others).

                                                   3 June 2011                                        checker(1)