Provided by: spark_2012.0.deb-11build1_amd64 bug


       checker - SPARK Proof Checker


       checker [OPTIONS] [FILE]


       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.


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

       -help  Show summary of options.

              Display version information.

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

              Confirmation needed to overwrite command or proof log files.

              Specify file name for the command log file.

              Specify file name for the proof log file.

              Execute a previously generated command log file.

              Resume a previously saved session.


              Checker rules database.


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


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

                                           3 June 2011                                 checker(1)