search

freespek / ssf-mc

EF project Exploring Automatic Model-Checking of the Ethereum specification
Apache License 2.0
3 stars 0 forks source link

Add an Alloy spec of FFG #50

Closed konnov closed 2 weeks ago

konnov commented 3 weeks ago

This is another attempt at pinpointing the bottlenecks in model checking the FFG spec. In theory, Alloy seems to be better suited for graph-theoretic problems. We have to collect the experimental data. In the preliminary results, Alloy also works for very small parameters.

konnov commented 2 weeks ago

Merging this spec, since we are not introducing any changes to it any longer. The only question is factored out in the issue #54