Pinned Loading

1. YUP YUP Public

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

   OCaml 36 4

2. Hobbit Hobbit Public

   Higher-Order Bounded Bisimulation Tool

   OCaml 5

3. pcfeq pcfeq Public

   Bisimulation Checking tool for PCFv programs

   OCaml 2

4. HOLiK HOLiK Public

   HOLi symbolic execution game semantics using the K semantic framework

   Racket 1

5. Hobbit-PDNF Hobbit-PDNF Public

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

   OCaml 1

6. YulTracer YulTracer Public

   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.

   OCaml 1