projects I've worked on
formal logic
- SMACCM
high-assurance software for autonomous vehicles - Trustworthy Systems
formal, code-level proofs for systems over 1 million lines of code - L4.verified / seL4
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
