SMT-LIB Format for
Finite Lists, Sets, and Maps

Sets, lists, and maps are elementary data structures used in most programs. Program analy­sis tools therefore need to decide verification conditions containing variables of such types. We propose a new theory for the SMT-Lib standard as the standard format for such for­mulae.

We provide:

For questions about the theories or the converter, contact Philipp Ruemmer.

SMT-LIB 2 Converter

To ease the adoption of the new theories and allow experiments, we have developed a pre­liminary axiomatisation of the theories in the SMT-LIB 1 language, together with a converter that translates SMT-LIB 2 problems into the SMT-LIB 1 format. Although the con­verter still has certain restrictions (that we will eliminate as soon as possible), it supports most parts of the SMT-LIB 2 format, all of the proposed list/set/map theories, comes with full type checking, and provides a good impression of how the theories can be used in practice.

The parser of the converter is written using the BNF Converter tool (in the source dis­tri­butions below, the grammar is defined in the file src/smtlib.cf). This grammar can be used to generate SMT-LIB 2 parsers for various languages, including C, C++ (the language of the converter), Java, and OCaml.

Releases

CBMC for SMT-LIB Version 2

We also provide a version of CBMC with prototypical support for generating formulas in the SMT-LIB version 2 format. Use the command line options

--smt2 --outfile dest

to write the verification conditions in SMT-LIB version 2 format into the file dest. The CBMC manual is here.

Releases