search

freespek / ssf-mc

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

Inductive invaraint #44

Closed Kukovec closed 4 weeks ago

Kukovec commented 1 month ago

Introduces inductive invariant fragments related to graph topology and the relation closure, as well as votes and justifications.