Posts
A Primer on Boolean Satisfiability
First steps to adding the magic of SAT to your problem-solving toolbox.
News
Our paper on push-button verification of an OS kernel will appear at SOSP 2017.
Our paper on the SpaceSearch library for building verified solver-aided tools will appear at ICFP 2017.
Our paper on synthesizing memory models will appear at PLDI 2017.
Gave the keynote at Clojure/West 2017.
Received an NSF CAREER Award.
Our paper on push-button verification of file systems won a best paper award at OSDI 2016.
Gave the keynote at RacketCon 2016.
Our paper on automated reasoning for web layout will appear at OOPSLA 2016.
Our paper on scalable verification of BGP configurations will appear at OOPSLA 2016.
Our paper on push-button verification of file systems will appear at OSDI 2016.
Released Rosette 2.2: now with support for quantified formulas!
Gave the Junior DN Prize Lecture at ECOOP 2016.
Released Rosette 2.1: now with push/pop incremental solving.
Our paper on verifying a radiotherapy machine will appear at CAV 2016.
Released Rosette 2.0: new theories, better performance!
Received a Sloan Research Fellowship.
Our paper on file system crash-consistency models will appear at ASPLOS 2016.
Our paper on fast synthesis of fast collections will appear at PLDI 2016.
Won the AITO Dahl-Nygaard Junior Prize.
Our paper on optimizing synthesis with metasketches will appear at POPL 2016.