Daniel Matichuk

Research & Engineering

I’m a software research engineer with a background in interactive theorem proving. I’m interested in practical applications of formal methods, specifically in developing automated reasoning tools and programming language features for proving software correctness. I enjoy using both theory and engineering in order to solve deep technical problems.

In my spare time I’m usually playing board games, video games, watching movies, or going for walks in parks around Portland.

Background

Daniel received his undergraduate degree in Computer Science from the University of Alberta before working as a research engineer on the seL4 microkernel verification project (https://ts.data61.csiro.au/projects/seL4-verification/). He then completed his PhD at the University of New South Wales, where he developed a framework for using automated reasoning to assist in building Isabelle proofs at scale.
At Galois, Daniel has been developing on a formal semantics of the Aarch32 ARM architecture for binary analysis, and more recently has started work on increasing the assurance level of verified Dafny programs.
Email Daniel Matichuk

Stay Connected