# Absynth.jl

Algebra-based loopsynthesizer

Absynth is a Julia package for synthesizing loops from a given polynomial loop invariant.

## Quick start

```
julia> ] add Absynth
julia> using Absynth
```

Absynth makes use of SMT solving at its core. As such you should have an SMT solver like Z3 or Yices installed.

You can check if Absynth can find Z3 or Yices by trying to call the constructor of the solver, that is, `Z3()`

or `Yices()`

. If this does not throw an error, then Z3 and/or Yices are available.

Then we can create a loop invariant which is allowed to be a Boolean combination of polynomial equations.

`julia> I = @invariant a == b^2`

The result of calling `synth`

is in fact a first-order recurrence system.

```
julia> recsys = synth(I, solver=Z3Solver)
RecSystem of size 3:
⎛ a(n+1) ⎞ ⎛ 1 2 1 ⎞⎛ a(n) ⎞ ⎛ a(0) ⎞ ⎛ 1//16 ⎞
⎜ b(n+1) ⎟ = ⎜ 0 1 1 ⎟⎜ b(n) ⎟ ⎜ b(0) ⎟ = ⎜ -1//4 ⎟
⎝ _c(n+1) ⎠ ⎝ 0 0 1 ⎠⎝ _c(n) ⎠ ⎝ _c(0) ⎠ ⎝ 1 ⎠
```

We turn the recurrence system into a loop by calling `loop(recsys)`

.

```
julia> loop(recsys)
quote
a = 1//16
b = -1//4
while true
a = a + 2b + 1
b = b + 1
end
end
```

## Publications

- A. Humenberger, N. Bjørner, L. Kovács. Algebra-based Loop Synthesis. In
*Integrated Formal Methods (iFM)*, 2020. To appear.