cprover
Loading...
Searching...
No Matches
goto-checker
Collaboration diagram for 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:

  • Property
  • Goto Verifier
  • Incremental Goto Checker

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:

  • goto_trace_providert : If a violated property has been found then a trace can be retrieved from the incremental goto checker.
  • fault_localization_providert : If a violated property has been found then a likely fault location can be determined.
  • witness_providert : A witness can be output (for violated and proved properties).

The combination of these three concepts enables:

  • Verification algorithms can be used interchangeably. There is a single, small interface for our verification engines.
  • Verification results reporting is uniform across all engines. Downstream tools can use the reporting output without knowing which verification algorithm was at work.
  • Building variants of verification engines becomes easy. Goto verifier and incremental goto checker implementations are built from small building blocks. It should therefore be easy to build variants by implementing these interfaces instead of hooking into a monolithic engine.
  • The code becomes easier to maintain. There are N things that do one thing each rather than one thing that does N things. New variants of verification algorithms can be added and removed without impacting others.

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

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