CBMC
goto-checker

Folder goto-checker

Author
Peter Schrammel

The goto-checker directory contains interfaces for the verification of goto-programs.

There are three main concepts:

A property has a property_id and identifies an assertion that is either part of the goto model or generated in the course of executing the verification algorithm. A verification algorithm determines the status of a property, i.e. whether the property has passed verification, failed, is yet to be analyzed, etc. See property_infot.

A goto verifier aims at determining and reporting the status of all or some of the properties, independently of the actual verification algorithm (e.g. path-merging symbolic execution, path-wise symbolic execution, abstract interpretation). See goto_verifiert.

An incremental goto checker is used by a goto verifier to execute the verification algorithm. Incremental goto checkers keep the state of the analysis and can be queried by the goto verifier repeatedly to return their results incrementally. A query to an incremental goto checker either returns when a violated property has been found or the verification algorithm has terminated. See incremental_goto_checkert. Incremental goto checkers can provide additional functionality by implementing the respective interfaces:

The combination of these three concepts enables:

There are the following variants of goto verifiers at the moment:

There are the following variants of incremental goto checkers at the moment: