projects I've worked on
formal logic
- Trustworthy Embedded Systems
formal, code-level proofs for systems over 1 million lines of code - L4.verified
verifying a high-performance microkernel - AFP
the archive of formal proofs - Isabelle
generic theorem proving - Verificard
theorem proving for JavaCard
tools
- JFlex
the fast scanner generator for Java - Grace
generating graphical editors - AutoFocus
rapid prototyping for embedded systems
computer algebra
- Spock
fast algorithms for sparse polynomials
