Patrick Rondon

Total chrome dome.

Email

pat.rondon@gmail.com

I'm interested in tools and techniques for building reliable software. As a graduate student, my work focused on refinement type-based approaches to verifying memory safety and functional correctness which place a low annotation burden on the programmer.

I now work at Google NYC. While at UCSD, my advisor was the incredible Ranjit Jhala.

Dissertation

publications

Abstract Refinement Types (ESOP 2013)

with Niki Vazou and Ranjit Jhala

CSolve: Low-Level Program Verification via Liquid Types (CAV 2012)

with Alexander Bakst, Ming Kawaguchi, and Ranjit Jhala

Deterministic Parallelism with Liquid Effects (PLDI 2012)

with Ming Kawaguchi, Alexander Bakst, and Ranjit Jhala

DSolve: Verification via Liquid Types (CAV 2010)

with Ming Kawaguchi and Ranjit Jhala

Low-Level Liquid Types (POPL 2010)

with Ming Kawaguchi and Ranjit Jhala

Type-Based Data Structure Verification (PLDI 2009)

with Ming Kawaguchi and Ranjit Jhala

Liquid Types (PLDI 2008)

with Ming Kawaguchi and Ranjit Jhala

talk slides

Liquid Types

PLDI 2008

projects

CSolve

A verifier for C programs based on Low-Level Liquid Type inference.

DSolve

A verifier for OCaml programs based on Liquid Type inference and type-based data structure verification.