- git repositories
- Selected projects:
From scratch C implementations of a SAT solver (watched
literals), SMT solver (eager encoded arrays + bitvectors),
symex engine, static analyzer, and neural network training. All
are within a few hundred lines, max. Most are set up as labs
that I've taught in our lab-based advanced operating systems
- dietc: a
fork of the chibicc C compiler that desugars C, i.e., outputs
code in an extremely restricted subset of C designed for easy
analysis and source-to-source instrumentation. libdietc
provides examples of use.
a super-simple, single-file, one-dependency PySMT alternative
that supports portfolio solving, automatic incrementalization,
and persistent caching.
C implementations of some algorithms from Knuth's combinations book.
- main website