Getting started with program analysis in Datalog by building a simple backwards symbolic execution engine in DDlog & Rust.

Aurora automatically identifies the root cause of bugs found via fuzzing. Published at USENIX Security 2020

A bounded model checker for smart contracts, that can steal money. Published at USENIX Security 2020

Allows the user to guide the fuzzer through the state space of the target program. Published at Oakland S&P 2020

Release of Nautilus 2.0 with many new features

A fast binary coverage measurement tool based on AFL’s Qemu mode

An opinionated tool to create beautiful presentations containing complex animations.

Automatically infer grammar like fragments during normal feedback fuzzing to improve test coverage. Published at USENIX Security 2019.