heron

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:

Idea

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.

Example

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.

Code

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.

Contact

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

Acknowledgements

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).