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.
• A Very Small SAT Solver
• Modulus - building an SMT solver from the ground up.
• https://github.com/zutshi/ToySMT

Static Analyzer

• Semantics and application to program verification, https://www-apr.lip6.fr/~mine/enseignement/l3/2015-2016/project.html

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