cprover
goto-checker

# Folder goto-checker

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. If a violated property has been found then additional information (e.g. a trace) can be retrieved from the incremental goto checker (if it supports that). See incremental_goto_checkert.

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:

• stop_on_fail_verifiert : Checks all properties, but terminates as soon as the first violated property is found and reports this violation. A trace ends at a violated property.
• all_properties_verifier_with_trace_storaget : Determines the status of all properties and outputs results when the verification algorithm has terminated. A trace ends at a violated property.
• all_properties_verifiert : Determines the status of all properties and outputs verification results incrementally. In contrast to all_properties_verifier_with_trace_storaget, all_properties_verifiert does not require to store any traces. A trace ends at a violated property.
• cover_goals_verifier_with_trace_storaget : Determines the status of all properties, but full traces with potentially several failing properties (e.g. coverage goals) are stored and results reported after the verification algorithm has terminated. The reporting uses 'goals' rather than 'property' terminology. I.e. a failing property means 'success' and a passing property 'failed'.

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