tools

Here are some tool implementations I have been involved with.

YulTracer  – bounded safety checker and interpreter for Yul, based on game semantics.

github.com/LaifsV1/YulTracer

RAM-C  –  logic-based model checker for fresh-register automata.

github.com/HamzaBandukara/RAM-C

RABiT  –  bisimulation equivalence checker for fresh-register automata.

github.com/HamzaBandukara/FRABisim

Hobbit  –  bounded bisimulation equivalence checking tool for higher-order programs.

github.com/LaifsV1/Hobbit

DEQ  –  equivalence checker for deterministic fresh-register automata.

github.com/sjrsay/deq

Coneqct  –  equivalence checker for stateful Java-like programs. 

github.com/sjrsay/coneqct