ravencheck 0.1.0

Decidable verification of Rust code using relational abstraction.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

# `ravencheck`

`ravencheck` is a tool for symbolic verification of Rust code, using guaranteed-decidable SMT queries for predictable results.

## Usage

First, make sure you have the [CVC5](https://cvc5.github.io/) SMT
solver available. You should be able to run `cvc5 --version` in your
dev environment.

Then, to use `ravencheck`, add its GitHub repository as a dependency
in your Cargo.toml file:

```
# Cargo.toml
...
[dependencies]
ravencheck = { git = "https://github.com/cuplv/ravencheck" }
...
```

Alternatively, you can clone the repo and use its path on your
filesystem as the dependency:

```
# Cargo.toml
...
[dependencies]
ravencheck = { path = "path/to/cloned/repo" }
...
```

You will then use the `#[ravencheck::check_module]` macro on modules
in which you want to use verification. See
[examples/sets.rs](./examples/sets.rs) for an example.

## About

"Raven" is an acronym for *relationally-abstracted verification
encoding*, the technique that is used to reduce verification
conditions to a decidable fragment of first-order logic (specifically,
the Extended EPR fragment).