Skip to main content

The Caesar Tool

The caesar binary contains all of Caesar's functionality: verifying HeyVL files, checking entailments, running the LSP server, and translation support for model checking.

Print help: The command-line help information is much more detailed than this document. Run caesar --help for available subcommands and caesar --help verify for details on the verify subcommand.

Compile the caesar binary with cargo build --release. The executable can be found at target/release/caesar. In the following, we just write caesar for the executable. Omit --release for the a binary with less optimizations; the result will be in target/debug/caesar. More information in our installation guide.

Print tracing messages: Caesar uses the tracing library to print (debugging) information during its operation. Set the RUST_LOG environment variable to specify a filter, e.g. export RUST_LOG="caesar=debug" or export RUST_LOG="caesar::smt=trace". You can disable ANSI colors in the output with export NO_COLOR=1.

Subcommand caesar verify​

The caesar verify subcommand takes a HeyVL program as input and tries to determine whether it verifies.

Verify HeyVL files: caesar verify file1.heyvl file2.heyvl ... Adding --raw indicates that input files consist only of a sequence HeyVL statements and that no declarations such as procedures are expected.

Timeouts and memory limits: Set a timeout of 60 seconds using --timeout 60. Set a memory limit of 16000 megabytes with --mem 16000.

Slicing: Caesar's slicing is controlled by the following flags:

  • With the --no-slice-error flag, Caesar will not do slicing to obtain better error messages (error slicing enabled by default).
  • With the --slice-verify flag, Caesar will do slicing for verification (this is not enabled by default).

Print intermediate data:

  • With the --print-parsed flag, Caesar pretty-prints the HeyVL code after parsing.
  • With the --print-core flag, Caesar prints the HeyVL code after parsing, type-checking, and desugaring.
  • With the --print-theorem flag, Caesar prints the theorem that is encoded into SMT.
  • With the --print-smt flag, Caesar prints the SMT-LIB query for each verification task. You can also use --smt-dir DIR with a directory DIR to have Caesar write the SMT-LIB queries to files in DIR.
    • If raco read is installed, Caesar will auto-format the SMT-LIB code with it. This is very useful as Z3's default formatting is really confusing sometimes.
  • With the --probe flag, Caesar will print information from Z3 probes to standard error.

Subcommand caesar entailment​

The caesar entailment subcommand checks whether one coproc's verification condition entails one proc's verification condition. See Entailment Checking for more information.

More Topics​