LaifsV1/YulTracer LaifsV1/YulTracer

  • Stars
    star
    1
  • Language
    OCaml
  • License
    MIT License
  • Created 5 months ago
  • Updated 3 months ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
LaifsV1/YulTracer
github

LaifsV1

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

YulTracer is an interpreter and future symbolic execution engine for Yul written in OCaml with Z3 for symbolic reasoning and compiled using the Dune build system.

More Repositories

1

YUP

YUP is a proof checker that performs automatic checking of simple program-correctness proofs of functional programs through inductive and equational reasoning.
OCaml
36
star
2

Hobbit

Higher-Order Bounded Bisimulation Tool
OCaml
5
star
3

pcfeq

Bisimulation Checking tool for PCFv programs
OCaml
2
star
4

BMC-2

BMC-2 is a bounded model checking tool for higher-order functional programs with free variables of ground-type.
OCaml
2
star
5

HOLiK

HOLi symbolic execution game semantics using the K semantic framework
Racket
1
star
6

Hobbit-PDNF

Implementation of Pushdown Normal-Form Bisimulation based on the Hobbit bisimulation verification tool
OCaml
1
star