Rapid

Rapid is a program verifier that works by taking the program's axiomatic semantics expressed in first-order logic and using it to prove partial correctness with respect to a user supplied specification.

What inputs are supported?

Rapid currently takes as inputs programs in a simple language While. Assertions can be added using the full expressivenes of first-order logic in SMT-LIB syntax.

What properties can be verified?

Rapid can verify the partial correctness of a program with respect to a user supplied specification

What are the tool’s main techniques for the supported (input, property) pairs?

Invariant generation, first-order theorem proving

What external tools are used? (e.g., compilers, SMT solvers)

Vampire theorem prover which in turns makes use of Z3 SMT solver and MiniSAT SAT solver.

What is the tool’s URL?

https://github.com/vprover/rapid

Example(s)

Assorted example can be found at:

https://github.com/vprover/rapid/tree/main/examples

References

Georgiou, Pamina, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovács, and Giles Reger.
The RAPID Software Verification Framework.
FMCAD 2022, p. 255. 2022.
paper