I enjoy building secure and correct systems. I have built a number of static analysis and automated verification tools, with a recent focus on analysis of binaries.
Data structures that may be generally useful
- haggle [41 ⭐ 📖]: An efficient graph library for Haskell
- persistent-vector [28 ⭐ 📖]: Persistent vectors for Haskell based on array mapped tries
- robbed [4 ⭐]: A pure Haskell implementation of Reduced Ordered Binary Decision Diagrams (BDDs)
- ql-grep [13 ⭐]: A code search tool that implements CodeQL on the tree-sitter infrastructure
- build-bom [58 ⭐]: Dynamically discover the commands used to create a piece of software
- whole-program-llvm [732 ⭐]: A wrapper script to build whole-program LLVM bitcode files; note that I consider this to be obsoleted by
build-bom, which takes a more robust approach to the same problem - itanium-abi [13 ⭐ 📖]: An implementation of C++ name mangling for the Itanium ABI
- what4-serialize [0 ⭐]: Serialization/deserialization for What4 expressions
- crepitans [3 ⭐]: A tool for scriptable exploration of binaries
- dismantle [26 ⭐]: A library of assemblers and disassemblers derived from LLVM TableGen data
- portable-executable [3 ⭐]: Tools for working with the Windows Portable Executable (PE) file format
- semmc [40 ⭐]: Stratified synthesis for learning machine code instruction semantics
- macaw [256 ⭐]: Open source binary analysis tools.
- macaw-loader [4 ⭐]: Uniform interface to load a binary executable and get Macaw Memory and a list of entry points.
- renovate [49 ⭐]: A library for binary analysis and rewriting
- language-sleigh [8 ⭐]: A parser for the Sleigh language, which is used to represent ISA semantics in Ghidra
- mctrace [6 ⭐]: An implementation of DTrace for machine code
- ddmin [4 ⭐]: An implementation of delta debugging (ddmin) in Haskell
- surveyor [20 ⭐]: A symbolic debugger for C/C++ (via LLVM), machine code, and JVM programs
- binary-walkr [4 ⭐]: A tool for examining ELF binaries
Note that these are interesting and informative, but definitely not efficient enough to use in production
- satisfaction [2 ⭐]: A DPLL SAT solver written in Haskell
- datalog [105 ⭐]: A pure Haskell implementation of Datalog
- ifscs [4 ⭐ 📖]: An inductive form set constraint solver in Haskell
- satir [2 ⭐]: An implementation of a SAT solver in Rust
- lgtm.el [1 ⭐]: A code review UI for emacs that supports multi-repository changesets
- haskell-pragma.el [3 ⭐]: An emacs hydra to enable Haskell language extensions efficiently
- haskell-interactive-import.el [0 ⭐]: A Haskell function and minor mode for interactively adding imports to modules
- pipemacs [1 ⭐]: Pipe data from standard input to emacs