Emina Torlak

Orcid: 0000-0002-1155-2711

Affiliations:
  • Amazon Web Services, USA
  • University of Washington, Seattle, USA


According to our database1, Emina Torlak authored at least 58 papers between 2004 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization.
Proc. ACM Program. Lang., 2024

Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version).
CoRR, 2024

How We Built Cedar: A Verification-Guided Approach.
Proceedings of the Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, 2024

2023
A Pretty Expressive Printer.
Proc. ACM Program. Lang., October, 2023

A Pretty Expressive Printer (with Appendices).
CoRR, 2023

Synthesis-Aided Crash Consistency for Storage Systems.
Proceedings of the 37th European Conference on Object-Oriented Programming, 2023

2022
A formal foundation for symbolic evaluation with merging.
Proc. ACM Program. Lang., 2022

Testing Dafny (experience paper).
Proceedings of the ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18, 2022

2020
Noninterference specifications for secure systems.
ACM SIGOPS Oper. Syst. Rev., 2020

Fixing Code that Explodes Under Symbolic Evaluation.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel.
Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation, 2020

Summary-Based Symbolic Evaluation for Smart Contracts.
Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

Synthesizing JIT Compilers for In-Kernel DSLs.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
Precise Attack Synthesis for Smart Contracts.
CoRR, 2019

Scaling symbolic evaluation for automated verification of systems code with Serval.
Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

Swizzle Inventor: Data Movement Synthesis for GPU Kernels.
Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, 2019

2018
Symbolic types for lenient symbolic execution.
Proc. ACM Program. Lang., 2018

Finding code that explodes under symbolic evaluation.
Proc. ACM Program. Lang., 2018

Refinement Types for Ruby.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

A Framework for Computer-Aided Design of Educational Domain Models.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Nickel: A Framework for Design and Verification of Information Flow Control Systems.
Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation, 2018

Generalized data structure synthesis.
Proceedings of the 40th International Conference on Software Engineering, 2018

2017
SpaceSearch: a library for building and verifying solver-aided tools.
Proc. ACM Program. Lang., 2017

Hyperkernel: Push-Button Verification of an OS Kernel.
Proceedings of the 26th Symposium on Operating Systems Principles, 2017

Synthesizing memory models from framework sketches and Litmus tests.
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Synthesizing interpretable strategies for solving puzzle games.
Proceedings of the International Conference on the Foundations of Digital Games, 2017

2016
SIMPL: A DSL for Automatic Specialization of Inference Algorithms.
CoRR, 2016

Optimizing synthesis with metasketches.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Fast synthesis of fast collections.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Push-Button Verification of File Systems via Crash Refinement.
Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, 2016

Scalable verification of border gateway protocol configurations with an SMT solver.
Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

Automated reasoning for web page layout.
Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

A Framework for Parameterized Design of Rule Systems Applied to Algebra.
Proceedings of the Intelligent Tutoring Systems - 13th International Conference, 2016

Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Specifying and Checking File System Crash-Consistency Models.
Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, 2016

2015

Toward a Dependability Case Language and Workflow for a Radiation Therapy System.
Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Toward tool support for interactive synthesis.
Proceedings of the 2015 ACM International Symposium on New Ideas, 2015

Crust: A Bounded Verifier for Rust (N).
Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, 2015

2014
What Gives? A Hybrid Algorithm for Error Trace Explanation.
Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

A lightweight symbolic virtual machine for solver-aided host languages.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

2013
Applications and extensions of Alloy: past, present and future.
Math. Struct. Comput. Sci., 2013

Growing solver-aided languages with rosette.
Proceedings of the ACM Symposium on New Ideas in Programming and Reflections on Software, 2013

Syntax-guided synthesis.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012
Scalable test data generation from multidimensional models.
Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), 2012

Synthesizing Programs with Constraint Solvers.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Angelic debugging.
Proceedings of the 33rd International Conference on Software Engineering, 2011

2010
MemSAT: checking axiomatic specifications of memory models.
Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010

Effective interprocedural resource leak detection.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Correct Refactoring of Concurrent Java Code.
Proceedings of the ECOOP 2010, 2010

2009
A constraint solver for software engineering: finding models and cores of large relational specifications.
PhD thesis, 2009

2008
Controlled physical random functions and applications.
ACM Trans. Inf. Syst. Secur., 2008

Finding Minimal Unsatisfiable Cores of Declarative Specifications.
Proceedings of the FM 2008: Formal Methods, 2008

2007
Kodkod: A Relational Model Finder.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

2006
Knowledge Flow Analysis for Security Protocols
CoRR, 2006

A Generalized Two-Phase Analysis of Knowledge Flows in Security Protocols
CoRR, 2006

2004
A type system for object models.
Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2004, Newport Beach, CA, USA, October 31, 2004

Faster constraint solving with subtypes.
Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2004


  Loading...