Tools

I spend most of my time tinkering with program analysis tools.

  • Crab: An abstract interpretation library for LLVM, contributed 4 novel domains for memory-access validation, object invariant inference, and heap-aware taint analysis
    • Most-Recently-Used Abstract Domain (MRUD): a memory domain for reason object invariants, with novel support for avoiding weak updates.
    • Symbolic Equality Abstract Domain (VarEq): an equality domain using union-find data structure to track equivalence classes of symbolic variables.
    • Template-Difference-Bound-Matrix Abstract Domain (TemplateDBM): a coeffeicient template domain for linear inequalities, especially for two-variable-per-inequality (TVPI) constraints.
    • Data-flow Tag Analysis over Recency Abstract Domain (DFA): a dataflow analysis for tracking tainted tags over heap objects, with domain reduction over memory domain.
  • SeaDSA: A points-to analysis for LLVM with interval-aware extensions for finer-grained object disjointness and pointer alias disambiguation
  • SeaBMC: A bounded model checker for LLVM; integrates Crab pre-analysis passes to prune provable assertions and speed up BMC encoding and SMT solving
  • Drift: An abstract-interpretation-based data flow refinement type inference tool — POPL 2021