Parameterized verification is a hard problem. Even more so, if we
consider parameterized systems with non-atomic checks of global
conditions. For example, an agent might check if all participants have
not raised a flag `b`

:

```
if for i = 0 ... N-1: b[i] == 0 then goto succ else fail
```

It turns out that interesting safety properties of prominent mutual exclusion algorithms can be proven by structural properties of the Petri net representation of instances of these algorithms. Using this observation we developed heuristics to find candidates of potential invariants for the parameterized systems from structural properties of instances.

In a second step we employ first-order theorem proving to check if these candidates indeed are inductive invariants of the parameterized system. For this, we rely on CVC4 and Vampire.

We implemented the proving procedure of finite instances, the
generalization heuristics, and the first-order verification of the
inductive invariants and safety properties in our tool
**heron**.

For example, the following example of a minimal version of Dijkstra's mutual exclusion algorithm can be proven by heron:

` ````
local b [false, true]
local pc [initial, toloop, loop, break, crit, done]
local p [0 - succ(N)]
transition pc(P1)=initial
-> b(P1)=true, pc(P1)=toloop
transition pc(P1)=toloop
-> p(P1)=1, pc(P1)=loop
transition pc(P1)=loop, p(P1)>N
-> pc(P1)=crit
transition pc(P1)=loop, p(P1)=0
-> p(P1)=succ(p(P1)), pc(P1)=loop
transition pc(P1)=loop, 1<=p(P1), p(P1)<=N, p(P1)=P1
-> p(P1)=succ(p(P1)), pc(P1)=loop
transition pc(P1)=loop, 1<=p(P1), p(P1)<=N, b(p(P1))=false
-> p(P1)=succ(p(P1)), pc(P1)=loop
transition pc(P1)=loop, 1<=p(P1), p(P1)<=N, p(P1)!=P1, b(p(P1))=true
-> pc(P1)=break
transition pc(P1)=break
-> b(P1)=false, pc(P1)=initial
transition pc(P1)=crit
-> pc(P1)=done
transition pc(P1)=done
-> b(P1)=false, pc(P1)=initial
critical pc(P1)=crit
```

It is essential for the mutual exclusion property here that for every
two agents at least one has not yet iterated over the other. This fact
corresponds to a trap involving the current value of the program
counter `pc`

, the value of the variable `b`

and
the iteration pointer `p`

.

heron is written in Python. The code is maintained on the GitLab of the TUM.

Since heron is subject to ongoing research the codebase is unstable. Please refer to the artifact for a stable snapshot.

If you have questions regarding heron, please contact Christoph, Mikhail, or Javier.

This project has received funding from the European Research Council (ERC) under the European Unions Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).