PyVCG 1.0.1

Verification Condition Generator

Verification Condition Generator

PyVCG is a utility library to generate VCs directly for CVC5 or standard-compliant SMTLIB2. The interface is deliberately generic and it should be easy to add API support for other solvers in the future.

This is pretty limited for now as the initial target is the expression language of TRLC.

Features

This library provides a wrapper around SMTLIB with some additional features:

• SMTLIB Scripts
• Automatic (minimal) logic discovery
• Basic sorts: Bool, Int, Real, and String
• Parametric sorts: Sequences
• Datatype sorts: Enumerations and Records
• Uninterpreted functions
• Quantifiers
• Boolean expressions: not, and, or, xor, implication
• If-then-else expressions
• Comparisons: =, <, >, <=, >=
• Int -> Real conversion
• Real -> Int conversion (smtlib rounding (round-to-negative) and arithmetic rounding (round-nearest-away))
• Unary arithmetic: -, abs
• Binary Int arithmetic: +, -, *, smtlib div, smtlib mod, python div, ada remainder
• Binary Real arithmetic: +, -, *, /
• String operations: length, contains, prefix, suffix, concatenation
• Sequence operations: length, contains, access, concatenation
• Record operations: access

In addition this library provides a graph to build VCs with multiple paths; and generating VCs for all paths. FastWP and higher-level modelling for language features (e.g. ite, loops) are planned later.

Drivers

Current support for outputs:

• SMTLIB (for writing and debugging)
• CVC5 API (for solving)

Dependencies

Run-time

• Python >= 3.9
• cvc5

Development

• GNU Make
• coverage
• pycodestyle
• pylint

Copyright & License

The sole copyright holder is Florian Schanda.

This library is licensed under the GNU GPL version 3 (or later).