John Matthews

This is a really basic web page I keep at Portland State University describing what I'm about these days.

Chronology

• I am currently working 80% time at Galois, Inc., a company specializing in high assurance software for security-critical applications. I spend 20% of my time at the Portland State University as an Adjunct Assistant Professor in the Computer Science Dept.

• From May 2004 to May 2007 I was on entrepreneurial leave from the CSEE department at the OGI School of Science and Engineering, part of the Oregon Health & Science University. During my leave I was also working 80% time at Galois, and 20% time at OGI/OHSU.

• From September 2002 to May 2004 I worked full-time as an assistant professor at the CSEE department of OGI/OHSU.
• From September 2000 to August 2002 I researched formal verification technology and applications at what is now HP-Lab's Cambridge Research Laboratory.

• In October of 2000 I received a Ph.D. in Computer Science from the Oregon Graduate Institute.

• In 1990 I received a B.S. in CS, Math, and Statistics from the University of Washington

Contact Information

Current Research Interests

Scaling-up formal verification. I am primarily interested in making theorem provers powerful enough to formally verify security- and safety-critical software. At Galois we are combining theorem proving and model checking technology to obtain high confidence that an implementation satisfies its specification for all possible system behaviors. Many of these applications are too large to be handled effectively by either theorem proving or model checking alone. However, it is often possible to use theorem proving tactics to abstract and decompose correctness properties of large designs into a series of verification conditions over smaller finite state machines. Each of these verification conditions can then be automatically verified using model checking.

Most recently we have been applying this approach to verify that C code is memory-safe (e.g. no buffer overflow flaws).

HOL as a formal modeling language. I am also interested in increasing the expressiveness of higher order logic, and using a subset of it as a high-level executable specification language that can also be formally reasoned about in a theorem prover. As one example, my dissertation describes a generalization of well-founded recursion in higher order logic, called converging equivalence relations (CERs). CERs can be used to define a large class of recursive functions over coinductive types, such as lazy lists and trees. Previous methods required one to define such functions co-recursively, or placed syntactic restrictions on the form definitions could take. I would like to integrate CER definition mechanisms more closely into existing theorem provers such as Isabelle, so that formal models written in higher order logic can be directly translated into lazy functional languages such as Haskell and executed.

PhD Research

As a PhD student at OGI I was a member of the Pacific Software Research Center. My research revolved around the Hawk project. My advisor was John Launchbury, who headed the project. I used the theorem prover Isabelle to verify the correctness of microprocessor specifications written in Hawk, and to perform correct source-to-source transformations of Hawk programs.

Publications