Mike Dodds
I’m a Principal Scientist at Galois, Inc, a private research consultancy based in Portland OR. Galois specializes in formal methods, programming languages, and systems assurance.
I’m interested in the real-world applications of formal methods:
- ‘Formal methods’: My work applies mathematical reasoning to ensure software is secure, correct, and bug-free. I’m interested in solving problems in high-impact domains like cryptography, distributed systems, concurrency, and hardware semantics.
- ‘Real-world’: I’m interested in building tools that can be deployed in software engineering environments. This means building powerful, reliable, and understandable tools that complement existing engineering workflows.
Projects I’m involved with:
- CN, a unified testing and verification tool for real C code.
- Daedalus, a safe parsing language we developed on the DARPA SafeDocs project. We used Daedalus to build a reference PDF parser for the PDF association.
- c2rust, a transpiler from C to Rust which is used for several popular Rust crates.
- Verified cryptography with our tools SAW and Cryptol. I’ve worked (amongst others) with AWS, including verifying core bits of the AWS-LibCrypto library.
Career history:
- 2004-2008: PhD student in the University of York, UK, working with Detlef Plump.
- 2008-2012: Postdoc in the Computer Laboratory, University of Cambridge, working with Matthew Parkinson and Peter Sewell.
- 2012-2017: Lecturer (approximately, an associate professor) in the University of York, UK.
- 2017-present: Principal Scientist at Galois, Inc.