Some open-source projects I worked on at Draper:
-
VIBES is a patch
compiler. It compiles source-level code fragments, edits them into
existing binaries, and formally verifies that the resulting binary has
only the intended changes.
-
CBAT is a
collection of binary analysis tools built on CMU's Binary Analysis
Platform (BAP). CBAT includes an SMT-based weakest precondition
analysis for BAP and various features for using it to analyze a single
program or compare the behavior of two programs. Documentation and a
tutorial are available on
the CBAT
website.
-
The HOPE
project built a variety of tools to support a security coprocessor
under development at Draper and Dover Microsystems. I contributed to
many pieces, including the design and implementation of
a language
for
expressing security
policies that can be enforced by the system.
-
PARTS is a
parser combinator library in Coq that supports abstraction to OCaml. It
achieves excellent performance via partial evaluation.
-
Cspgen is a
tool for creating models of software in the Communicating Sequential
Processes (CSP) process calculus. The tool accepts both C programs and
LLVM IR as input, and writes a corresponding .csp file to disk. The
output is compatible with FDR3, the Oxford CSP model checker. FDR may be
used to check the model for for general properties, like deadlock
freedom, divergence freedom and determinism, or may be compared with
specifications written in CSP using refinement.
-
Specgen is a
tool for creating models of Enterprise Architect statecharts in the
Communicating Sequential Processes (CSP) process calculus. The output
is compatible with FDR3, the Oxford CSP model checker.
Older projects:
-
I wrote hcross, a
cross-platform, open source Haskell application for interactively
solving crossword puzzles. It's effectively a free Across
Lite replacement.
-
As part of the Software Foundations project, I made a number
of contributions to coqdoc, the documentation tool
for the Coq proof assistant.
-
I have contributed to and
maintain libpuz, a
C library for handling the Across Lite crossword puzzle file
format. I have also participated in the community effort to
reverse engineer and document that format, located at the same
Google Code project page.
-
I wrote
hpuz, the
Haskell bindings for the libpuz library.
-
In 2007, I participated in Jane Street
Capital's OCaml Summer
Project. This was a great experience, and I highly recommend it.
My project
was pcl, a
port of Haskell's popular Parsec library (monadic parser combinators) to
Ocaml. Don't use this in production code - there are now much better
options for parser combinators in OCaml.