I am currently the VP Research & Development at Certora, Inc.. In this capacity, I have found multiple bugs in the Solidity compiler’s output, which you can read all about on medium. This is my personal/academic homepage; if you want to reach out about smart contracts or the blockchain: don’t.
I was formerly a post-doctoral researcher at Kyoto University in the lab of Prof. Atsushi Igarashi. I graduated with a PhD in March 2019 from the Computer Science and Engineering department at the University of Washington.
I worked in the PLSE group and I was advised by Dan Grossman. I’ve also collaborated with Emina Torlak.
Most recently I worked on the automated verification of object-oriented programs. More generally my research has focused on using program analysis to solve practical software engineering problems and improving the soundness and precision of analyses on difficult-to-analyze, framework-based applications. My research vision is outlined in my SNAPL ‘17 paper.
My prior research has used static analysis to find consistency errors in programs that interact with dynamic execution environments, techniques from model checking to check for memory safety errors in Rust, dynamic taint analysis to find bugs in dynamic configuration update schemes, and type systems and program instrumentation to find type errors in Ruby programs. You can find links to all of my publications below, or look at my CV.
I received my BS in Computer Science at the University of Maryland, College Park. My honors project - which helped develop an undergraduate PL curriculum - was advised by Dr. Jeffrey Foster. I also had the pleasure of working with Dr. Michael Hicks.
Publications
Consort: Context-and flow-sensitive ownership refinement types for imperative programs
John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, and Naoki Kobayashi. In ESOP ‘20
Paper (PDF) | Springer
Learning to Adapt: Analysis for Configurable Software
John Toman. PhD Dissertation.
Dissertation (PDF)
Concerto: A Framework for Combined Concrete and Abstract Interpretation
John Toman and Dan Grossman. In POPL ‘19.
Paper (PDF) | ACM | GitHub | Web
Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates.
John Toman and Dan Grossman. In ECOOP ‘18.
Paper (PDF) | GitHub | Web | Artifact
Taming the Static Analysis Beast.
John Toman and Dan Grossman. In SNAPL ‘17.
Paper (PDF) | Web
Staccato: A Bug-Finder for Dynamic Configuration Updates.
John Toman and Dan Grossman. In ECOOP ‘16.
Winner: Distinguished Artifact Award
and Distinguished Poster Award.
Paper (PDF) | GitHub | Web | Talk (YouTube) | Artifact
CRust: A Bounded Verifier for Rust.
John Toman, Stuart Pernsteiner, and Emina Torlak. In ASE ‘15.
Paper (PDF) | GitHub | Web
The Ruby Type Checker.
Brianna M. Ren, John Toman, T. Stephen Strickland, and Jeffrey Foster.
In SAC ‘13.
Paper (PDF) | Web
Blog Posts
- 16 Apr 2020 » I Hate Kotlin
- 13 Nov 2018 » Splitting a PDF with Table of Contents
- 18 Oct 2018 » Fun with Lattices
- 20 Sep 2018 » Fun with Fixpoints
- 20 Aug 2018 » Instrumenting the Trade* Benchmarks in DaCapo