Emina Torlak

Our paper on data movement synthesis for GPU kernels will appear at ASPLOS 2019.

Our paper on symbolic profiling won a Distinguished Artifact Award at OOPSLA 2018.

Released Rosette 3.0: new performance engineering tools and new solvers!

Our paper on symbolic profiling for solver-aided languages and frameworks will appear at OOPSLA 2018.

Our paper on the Nickel framework for design and verification of information flow control systems will appear at OSDI 2018.

Gave a keynote on solver-aided programming at ISSTA 2018.

Gave a two-day course on Rosette at the Eighth Summer School on Formal Techniques (SSFT 2018).

Got tenure!

Our paper on generalized data structure synthesis won an ACM SIGSOFT Distinguished Paper Award at ICSE 2018.

Our paper on generalized data structure synthesis will appear at ICSE 2018.

Our paper on computer-aided design of educational domain models will appear at VMCAI 2018.

Our paper on refinement types for Ruby will appear at VMCAI 2018.

Our paper on automatic formal verification for EPICS will appear at ICALEPCS 2017.

Our paper on symbolic types for lenient symbolic execution will appear at POPL 2018.

Our paper on push-button verification of an OS kernel will appear at SOSP 2017.

A Primer on Boolean Satisfiability

First steps to adding the magic of SAT to your problem-solving toolbox.

Our paper on synthesizing puzzle-solving strategies will appear at FDG 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.

Clojure/West 2017 interview by PurelyFunctional.tv.

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!

Our paper on synthesizing tutoring rules for K-12 algebra will appear at ITS 2016.

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.