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) at the University of York, UK.
• 2017-present: Principal Scientist at Galois, Inc.