Sotabase

Career

· Senior Principal Scientist, Amazon Web Services (AWS)2021–
· Associate Professor, university2018–2023
· Assistant Professor, University of Washington2014–2018
· Assistant Research Engineer, UC Berkeley2012–2014
· Senior Computer Scientist, LogicBlox2011–2011
· Research Staff Member, IBM2008–2011
· Ph.D., Computer Science, Massachusetts Institute of Technology2003–2009
· M.Eng., Computer Science, Massachusetts Institute of Technology2002–2004
· B.Sc., Computer Science, Massachusetts Institute of Technology1998–2002

Publications (80)

Syntax-guided synthesis
Formal Methods in Computer-Aided Design · 2013
871
cited
Kodkod: A Relational Model Finder
International Conference on Tools and Algorithms for Construction and Analysis of Systems · 2007
544
cited
A lightweight symbolic virtual machine for solver-aided host languages
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2014
257
cited
Growing solver-aided languages with rosette
SIGPLAN symposium on New ideas, new paradigms, and reflections on programming and software · 2013
251
cited
Angelic debugging
International Conference on Software Engineering · 2011
143
cited
This Paper Is Included in the Proceedings of the 12th Usenix Symposium on Operating Systems Design and Implementation (osdi '16). Push-button Verification of File Systems via Crash Refinement Push-button Verification of File Systems via Crash Refinement
125
cited
Controlled physical random functions and applications
TSEC · 2008
120
cited
Scaling symbolic evaluation for automated verification of systems code with Serval
Symposium on Operating Systems Principles · 2019
118
cited
Hyperkernel: Push-Button Verification of an OS Kernel
Symposium on Operating Systems Principles · 2017
117
cited
Artifact
Artifact Digital Object Group · 2018
110
cited
Finding Minimal Unsatisfiable Cores of Declarative Specifications
World Congress on Formal Methods · 2008
95
cited
Optimizing synthesis with metasketches
ACM-SIGACT Symposium on Principles of Programming Languages · 2016
94
cited
MemSAT: checking axiomatic specifications of memory models
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2010
87
cited
Specifying and Checking File System Crash-Consistency Models
International Conference on Architectural Support for Programming Languages and Operating Systems · 2016
83
cited
Scalable verification of border gateway protocol configurations with an SMT solver
Conference on Object-Oriented Programming Systems, Languages, and Applications · 2016
80
cited
A constraint solver for software engineering: finding models and cores of large relational specifications
2009
76
cited
Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel
USENIX Symposium on Operating Systems Design and Implementation · 2020
67
cited
Synthesizing memory models from framework sketches and Litmus tests
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2017
62
cited
Effective interprocedural resource leak detection
2010 ACM/IEEE 32nd International Conference on Software Engineering · 2010
61
cited
Computer Aided Verification
Lecture Notes in Computer Science · 2016
60
cited
Sotabase
Emina Torlak | Researcher Profile | Sotabase | Sotabase