gleiss / rapid

Software Verification tool, which uses superposition-based theorem proving to establish the functional correctness of array- and hyper-properties.

Overview

RAPID is a software verification tool that takes a program together with a property as input and produces a first-order-encoding of correctness in SMTLIB syntax. This encoding can then be passed to an arbitrary first-order reasoning engine which supports SMTLIB, e.g. Vampire.

RAPID is focused on

• programs containing arrays
• functional properties, hyperproperties, possibly with quantifier alternations
• proving properties instead of disproving them (we don't try to find bugs)

Using RAPID

RAPID is intended to be used as follows:

• Write your program in the supported while-language,
• Write the property you want to prove in the supported SMTLIB-syntax,
• Pass the file containing the program and the property to RAPID, which generates an SMTLIB-encoding.
• Pass the file containing the SMTLIB-encoding to Vampire

Building the executable

There are two steps involved in building RAPID.

First, we generate the source-code files for the RAPID-parser using Flex and Bison: Make sure you have these two tools installed and that the paths are properly set in parser_generator/Makefile. Then, while being in parser_generator, run make (which produces the necessary files in src/parser/).

Secondly, we use CMake to generate the necessary files which are needed while building RAPID. Make sure you have CMake installed.

Starting from the main directory, make a new folder (to do an out-of-source-build) and switch to it by running

$ mkdir build; cd build

The next step depends on your favourite build tool:

If you want to use make as build-tool, run

$ cmake ..

and build RAPID by running

$ make

If you want to use XCode as build-tool, run

$ cmake -G Xcode ..

and build RAPID from the generated XCode project (which will be generated in /build/)

For other build-tools like ninja, Visual Studio, Eclipse or Sublime2, consult the CMake documentation.

Which programs and properties may be used as input?

The programs must be given in a dedicated while-like language. We support integer- and integer-array-variables, the standard statements (assignments, if-else, while, skip) and assertions of the program (in SMTLIB-format).

See the example programs on the repository for more details.

Which first-order theorem prover should I use?

Short answer: Vampire

Long answer: Any prover that supports SMTLIBv2.6-syntax can in principle be used to solve problems generated by Rapid. In practice the solver should have efficient support for quantifiers, in particular for quantifier-alternations. The encoding is optimized for superposition-based provers, and in particular for Vampire.

rapid's Issues

Better error-reporting in Parser

Refactor assertion violations into meaningful parser feedback.
Most important in practice: Feedback if term-symbol-argument-sorts and term-subterm-sorts differ.

Improve Parser to handle function calls

Main goal:

• Allow to write smart-contract-like programs with function calls.

add option to exclude lemmas from output

Would be nice to have a command line option to only generate the program semantics and the property as lemmas are not used for trace properties atm.

Support for Boolean Variables

Implement copy(label) for Formula

Should return a copy of the formula, with label as label.

Add gcc build support

Because of its in that regard stricter interpretation of the C++ standard gcc (together with libstdc++) is currently not able to successfully build the the project. It fails, because of std::vector declarations with const values in the class Problem.

20 Benchmarks

Refactor 20 of the old benchmarks into the Spectre format.

Support for multiple conjectures

• generalize the parser to support multiple conjectures
• output one smtlib-encoding of semantics/lemmas/conjecture per conjecture

Advantages:

• It is quite natural to formulate multiple conjectures for the same program, so we want to support it.
• Currently each conjecture we want to prove requires a copy of the program, which is involved (in particular if one discovers a bug in the program and needs to fix it in each copy).

Add support for If-statement (without else)

• Currently, we directly only support if-else.
• We expect to have many programs where we want to use if without else.
• We can also use if-else with a skip statement in the else-branch, but it is inconvenient to do so.

Const Variables

Requires #2 and #3.

Add support for const variables.

• Figure out syntax (probably const vars as default and var keyword for non-const vars)
• Implement parsing
• Implement semantics: Only add value-equalities for non-const vars

Advantages:

• Simplifies semantics
• Simplifies reasoning, removes need for a simple case of induction.

Implement Trace Lemmas

Adopt the trace lemmas from QuIt to the new Spectre setting: We have a new syntax, but more crucially we support a much more expressive language, with multiple locations and nested program statements.

Support for Arrays of Booleans

Allow Var-decls everywhere

Generalize current implementation, which only allows Var-decls at the beginning of each function

• Generalize Parser
• Generalize semantics: Don't need to add variable-equalities, if the variable is not defined yet.

Improve Parser to handle multiple function definitions

Fix Lemma asserting n(t1)=n(t2)

Crashes if loop is nested in other loop, forgot to quantify over enclosingIterator-vars.