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: