toy projects

Theorem Prover

• Designing a Theorem Prover, Lawrence C Paulson, slides
  • Implementation in OCaml, https://github.com/jubnzv/folderol

SMT

• SAT-MICRO: petit mais costaud! - Sylvain Conchon, Johannes Kanig, Stéphane Lescuyer, https://inria.hal.science/inria-00202831/document
  • Haskell version, https://hackage.haskell.org/package/sat-micro-hs
  • OCaml version, https://gist.github.com/Drup/4dc772ff82940608834fc65e3b80f583
• Semantics and applications to verification - Sylvain Conchon, Antoine Miné and Xavier Rival, https://www.di.ens.fr/~rival/semverif-2016/
  • toy-smt in OCaml, https://github.com/Ekdohibs/toy-smt
• A poor man’s MaxSMT, https://yurichev.com/blog/maxsmt/
• SMT Solvers: Theory and Implementation, https://leodemoura.github.io/files/oregon08.pdf
• Internals of SMT Solvers, https://leodemoura.github.io/files/SATSMT2013.pdf
• kissat is an SMT solver written by Armin Biere on a plain C. Simple enough for understanding.
• SATurne - is a simple, purely functional SAT solver written and verified in Coq. It's a tiny solver, absolutely not designed for performances nor scalability. It is, however, intended to be well-documented, easy to understand and extremely trustworthy.
• Modulus - building an SMT solver from the ground up.
• https://github.com/zutshi/ToySMT - is a small SMT solver made by Denis Yurichev. It supports only booleans and bitvecs. No integers, let alone reals and arrays and tuples and whatever.
• SATurne -a tiny verified SMT solver.

SAT

• A Very Small SAT Solver
• https://github.com/marijnheule/microsat
• lsat

Static Analyzer

• Semantics and application to program verification. The goal of the project is to implement a small static analyzer by abstract interpretation for a simple language. Slides, Project page
• UNO

Model Checker

• Build your own model checker in one month - Jin Song Dong, Jun Sun, https://ieeexplore.ieee.org/document/6606751
• X.21 Analysis Revisited: the Micro-Tracer, AT&T Bell Laboratories, Technical Memorandum 11271-8710230-12, October 23, 1987. (PDF). Source code - https://spinroot.com/gerard/micro.html

Fuzzing Engine

• Build simple fuzzer: part 1, part 2, part 3, part 4, part 5, part 6.
• Minimal symbolic model checker & fuzzer - https://github.com/xiw/mini-mc
• A very minimal implementation of the core idea of Hypothesis, https://github.com/DRMacIver/minithesis
• Writing the Fuzzer