# Solving Constrained Horn Clauses Using `shara`

Verifying that a given program satisfies a given *safety property*
(i.e., a property that specifies executions that should not happen)
can be reduced to solving a class of logic-programming problems called
*Constrained Horn Clauses* (CHCs). CHCs can express
safety-verification problems of imperative programs, recursive
programs, some concurrent programs, and functional programs.

`shara`

is a CHC solver. It operates purely on CHC systems, and does
not require them to correspond to programs in particular languages, or
particular safety properties.

## Determining satisfiability of a CHC system

For example, consider the following implementation of the Fibonacci function:

```
int fib(int n) {
int i = 2;
int prev = 1;
int cur = 1;
while (i < n) {
cur = prev + cur;
prev = cur;
i++; }
return cur;
}
```

Proving that `fib`

always returns a non-zero value can be reduced to
solving the following CHC system:

```
i = 2 /\ prev = cur = 1 => R5(prev, cur, i, n)
R5(n, i, prev, cur), i < n => R5(n, i + 1, cur, prev + cur)
R5(n, i, prev, cur), i >= n => cur != 0
```

where a *solution* is an interpretation of the *relational predicate
symbol* `R5`

as a formula over variables `n`

, `i`

, `prev`

, and `cur`

such that each of the entailments given above holds. One such solution
interprets `R5`

as `prev > 0 /\ cur > 0`

.

`shara`

, given such a system, reports that it has a solution.

## Determining unsatisfiability of a CHC system

Not every CHC system has a solution. In particular, for program `P`

and property `Q`

such that `P`

does not satisfy `Q`

, any CHC system
that corresponds to the problem of verifying that `P`

satisfies `Q`

will not have a solution.

For example, consider the following erroneous implementation of the Fibonacci function:

```
int buggy_fib(int n) {
int i = 2;
int prev = 0;
int cur = 0;
while (i < n) {
cur = prev + cur;
prev = cur;
i++; }
return cur;
}
```

The corresponding CHC system

```
i = 2 /\ prev = cur = 0 => R5(prev, cur, i, n)
R5(n, i, prev, cur), i < n => R5(n, i + 1, cur, prev + cur)
R5(n, i, prev, cur), i >= n => cur != 0
```

has no solution. `shara`

, given such a system, reports that it has no
solution.

## Building `shara`

`shara`

is implemented as an alternative version of the `z3`

automatic
theorem prover. To build, run the following commands in package’s
main directory `SHARA_DIR`

:

```
$ python scripts/mk_make.py
$ cd build
$ make
```

When successful, the build system generates an implementation

## Using `shara`

`shara`

, given a CHC system `S`

in SMT2 format, attempts to determine
if `S`

has a solution.

After building `shara`

in directory `SHARA_DIR`

, to determine if a CHC
system in file `chcs.smt2`

has a solution, run the command

```
$ SHARA_DIR/z3 chcs.smt2
```

## Implementation

`shara`

is implemented as a fork of the
`z3`

automatic theorem prover . It
supports an interface identical to that supported by the interface
supported by `z3`

4.5.

The internal behavior of `z3`

and `shara`

differ only when `shara`

is
given a CHC system. The entire implementation of `shara`

is
represented by alternative implementations of a solving algorithm used
within `z3`

’s solver.

### References

`shara`

implements a novel algorithm for solving *recursion-free*
CHCs, which is based on the observation that a novel class of
recursion-free CHCs can be solved efficiently. A technical report on
the algorithm implemented in `shara`

is publicly available.

Qi Zhou and William Harris. *Solving Constrained Horn Clauses Using
Dependence-Disjoint Expansions*. arxiv