Emina Torlak

Our paper on a formal foundation for symbolic evaluation will appear at POPL 2022.

Honored to receive the Robin Milner Young Researcher Award and give a talk at PLDI 2021.

Gave a talk on solver-aided verification for systems software at the Newton Institute workshop on verified software (VSOW04).

Gave a talk on Rosette and Jitterbug at the Northwestern University.

Released Rosette 4.0: a new runtime and new language features!

Gave a joint talk with Xi Wang on Rosette and Jitterbug at Algorand.

Gave a talk on Rosette and Jitterbug at the UMass CS Systems Lunch.

Gave a colloquium talk on Rosette and Jitterbug at the University of Iowa.

Our paper on summary-based symbolic evaluation for smart contracts won an ACM SIGSOFT Distinguished Paper Award at ASE 2020.

Our paper on applying formal methods to BPF just-in-time compilers in the Linux kernel will appear at OSDI 2020.

Our paper on summary-based symbolic evaluation for smart contracts will appear at ASE 2020.

Our paper on synthesizing JIT compilers for in-kernel DSLs will appear at CAV 2020.

Our paper on fixing performance bottlenecks in code under symbolic evaluation will appear at VMCAI 2020.

Our paper on scaling automated verification with Serval won a best paper award and a distinguished artifact award at SOSP 2019.

Luke, Xi, and I gave a tutorial on Serval at SOSP 2019.

Gave a talk on solver-aided programming at Facebook PLEMM 2019.

Gave a keynote on solver-aided programming at ICFP 2019.

Our paper on scaling automated verification using Serval will appear at SOSP 2019.

Gave a tutorial on solver-aided programming at CAV 2019.

Serving as the Program Chair for PLDI 2020.

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.