Skip to content

Releases: franck44/evm-dis

First release with CFG verification

21 Nov 02:27
Compare
Choose a tag to compare

In this release the following features are added:

  • support for verification of CFGs generated by the decompiler and CFG generator
  • stronger post-conditions in abstract semantics to verify CFGs
  • update to Dafny 4.9.0 for verification
  • benchmarks: verified CFGs for the test suite less_than_300_opcodes from the project EVMLisa

V0.1.0-beta

24 Jan 04:57
Compare
Choose a tag to compare
  • add formal verification of CFGs
  • fix minor typos in documentation.

v0.0.0-alpha

16 Jan 05:15
Compare
Choose a tag to compare
v0.0.0-alpha Pre-release
Pre-release

This release provides the following features:

  • build control flow graph for EVM bytecode
  • generates a proof that the CFG is correct in the form of a Dafny program.