CV

Education

• Ph.D in Version Control Theory, GitHub University, 2018 (expected)
• M.S. in Jekyll, GitHub University, 2014
• B.S. in GitHub, GitHub University, 2012

Work experience

• Spring 2024: Academic Pages Collaborator
  • Github University
  • Duties includes: Updates and improvements to template
  • Supervisor: The Users
• Fall 2015: Research Assistant
  • Github University
  • Duties included: Merging pull requests
  • Supervisor: Professor Hub
• Summer 2015: Research Assistant
  • Github University
  • Duties included: Tagging issues
  • Supervisor: Professor Git

Skills

• Skill 1
• Skill 2
  • Sub-skill 2.1
  • Sub-skill 2.2
  • Sub-skill 2.3
• Skill 3

Publications

Crux, a Precise Verifier for Rust and Other Languages

Macaw: A Machine Code Toolbox for the Busy Binary Analyst

Daedalus: Safer Document Parsing

Research Report: An Optim (l) Approach to Parsing Random-Access Formats

Trustworthy Runtime Verification via Bisimulation (Experience Report)

Formally Verifying Industry Cryptography

Verified Cryptographic Code for Everybody

On the Formal Verification of the Stellar Consensus Protocol

Compositional Verification of Compiler Optimisations on Relaxed Memory

Starling: Lightweight Concurrency Verification with Views

Proving Linearizability Using Partial Orders

Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic

Refining Existential Properties in Separation Logic Analyses

A Scalable, Correct Time-Stamped Stack

Learning Assertions to Verify Linked-List Programs

Towards Rigorously Faking Bidirectional Model Transformations

C/C++ Causal Cycles Confound Compositionality

Proof-Directed Parallelization Synthesis by Separation Logic

Ribbon Proofs for Separation Logic

Library Abstraction for C/C++ Concurrency

Resource-sensitive synchronization inference by abduction

Safe asynchronous multicore memory operations

A simple abstraction for complex concurrent indexes

jStar-eclipse: an IDE for automated verification of Java programs

Automatic safety proofs for asynchronous memory operations

Modular reasoning for deterministic parallelism

Concurrent Abstract Predicates

Explicit Stabilisation for Modular Rely-Guarantee Reasoning

Deny-Guarantee Reasoning

From Hyperedge Replacement to Separation Logic and Back

PhD Thesis: Graph Transformation and Pointer Structures

Graph Transformation in Constant Time

Extending C for Checking Shape Safety

Talks

N Things I Learned Trying to Do Formal Methods in Industry

October 09, 2024

Workshop talk at Big Specification Workshop 2024, Isaac Newton Institute, Cambridge, UK

LLMs are Useful for Small Problems

May 06, 2024

Workshop talk at HCSS 2024, Annapolis, MD

Parsing and Understanding in a Messy World

January 31, 2024

Research seminar at CSE Colloquium, UC Santa Cruz

How Do We Know Weak Memory Matters?

January 15, 2024

Workshop talk at Future of Weak Memory Workshop 2024, London, England

Verified Cryptographic Code for Everybody

January 01, 2023

Research seminar at Strange Loop 2022,

Teaching

Service and leadership

• Currently signed in to 43 different slack teams