projects I've worked on
formal logic
- INSPECTA
Industrial Scale Proof Engineering for Critical Trustworthy Applications - CASE
Cyber Assured Systems Engineering - SMACCM
high-assurance software for autonomous vehicles - L4.verified and 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

