---
name: "checker"
section: "1"
platform: "linux"
package: "spark"
version: "2012.0.deb-11+b2"
release: "Debian 9 (Stretch)"
platforms: ["linux"]
url: "https://new.carta.tech/checker"
---

# checker(1)

SPARK Proof Checker

## 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)](/spark/1.md), [**sparksimp**(1)](/sparksimp/1.md), [**spadesimp**(1)](/spadesimp/1.md), [**pogs**(1)](/pogs/1.md).

## AUTHOR

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