## Absynth.jl

A Julia package for loop synthesis
Author ahumenberger
Popularity
7 Stars
Updated Last
7 Months Ago
Started In
March 2019

# Absynth.jl

Algebra-based loop synthesizer

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

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

### Required Packages

View all packages

### Used By Packages

No packages found.