This page contains a short chronological overview of my main projects.

Since I joined UC Berkeley (February 2010), I've been working on a number of software security and analysis projects. When I'll have more free time, I'll update this page with new projects... In the meantime, see publications.

# MACE (2010—?) — Model-inference-Assisted Concolic Execution

In this project, I'm looking into new approaches to software security and analysis based on grammar inference.

# Malware Analysis (2010—?) — A Formal Approach to Malware Analysis

This is one of the projects I'm working on at Berkeley. The focus is on researching how automata inference can help in detection and classification of malware.

# Calysto (2006—2008) — Scalable Software Static Checking

Fast static checker for checking large bodies of code. Exploits the structure at several levels of granularity, which significantly improves the scalability. Based on a novel symbolic execution algorithm and structural abstraction. Tight integration with the Spear theorem prover makes it exceptionally fast.

# Spear (2006—2008) — Fast Bit-vector Arithmetic Theorem Prover and SAT Solver

Fast bit-vector arithmetic (a.k.a. modular arithmetic, machine arithmetic) theorem prover and SAT solver. Supports all standard modular arithmetic operators, including signed/unsigned division and remainder. Supports several standard formats. Can be easily automatically optimized to a specific set of instances.

# HyperSAT (2004—2005) — Experimental Boolean Satisfiability Solver

Experimental B-cubing based solver. B-cubes are novel data structures for search space pruning.