Emina Torlak

ORCID

Publication Activity (10 Years)

Years Active: 2004-2024
Publications (10 Years): 37

Top Venues

CoRR

Proc. ACM Program. Lang.

VMCAI

PLDI

Massachusetts Institute of Technology, Cambridge, MA, USA (PHD)

Education History

Massachusetts Institute of Technology, Cambridge, MA, USA

PHD

Publications

Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John H. Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, Andrew Wells
How We Built Cedar: A Verification-Guided Approach. SIGSOFT FSE Companion (2024)
Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John H. Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, Andrew Wells
How We Built Cedar: A Verification-Guided Approach. CoRR (2024)
Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John H. Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, Andrew Wells
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version). CoRR (2024)
Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John H. Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, Andrew Wells
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. Proc. ACM Program. Lang. 8 (OOPSLA1) (2024)
Jacob Van Geffen, Xi Wang, Emina Torlak, James Bornholt
Synthesis-Aided Crash Consistency for Storage Systems. ECOOP (2023)
Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak
A Pretty Expressive Printer (with Appendices). CoRR (2023)
Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak
A Pretty Expressive Printer. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Sorawee Porncharoenwase, Luke Nelson, Xi Wang, Emina Torlak
A formal foundation for symbolic evaluation with merging. Proc. ACM Program. Lang. 6 (POPL) (2022)
Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamaric, Neha Rungta, Emina Torlak
Testing Dafny (experience paper). ISSTA (2022)
Yu Feng, Emina Torlak, Rastislav Bodík
Summary-Based Symbolic Evaluation for Smart Contracts. ASE (2020)
Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, Emina Torlak
Synthesizing JIT Compilers for In-Kernel DSLs. CAV (2) (2020)
Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, Xi Wang
Noninterference specifications for secure systems. ACM SIGOPS Oper. Syst. Rev. 54 (1) (2020)
Luke Nelson, Jacob Van Geffen, Emina Torlak, Xi Wang
Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. OSDI (2020)
Sorawee Porncharoenwase, James Bornholt, Emina Torlak
Fixing Code that Explodes Under Symbolic Evaluation. VMCAI (2020)
Phitchaya Mangpo Phothilimthana, Archibald Samuel Elliott, An Wang, Abhinav Jangda, Bastian Hagedorn, Henrik Barthels, Samuel J. Kaufman, Vinod Grover, Emina Torlak, Rastislav Bodík
Swizzle Inventor: Data Movement Synthesis for GPU Kernels. ASPLOS (2019)
Yu Feng, Emina Torlak, Rastislav Bodík
Precise Attack Synthesis for Smart Contracts. CoRR (2019)
Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang
Scaling symbolic evaluation for automated verification of systems code with Serval. SOSP (2019)
Stephen Chang, Alex Knauth, Emina Torlak
Symbolic types for lenient symbolic execution. Proc. ACM Program. Lang. 2 (POPL) (2018)
Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak
Refinement Types for Ruby. VMCAI (2018)
James Bornholt, Emina Torlak
Finding code that explodes under symbolic evaluation. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Eric Butler, Emina Torlak, Zoran Popovic
A Framework for Computer-Aided Design of Educational Domain Models. VMCAI (2018)
Calvin Loncaric, Michael D. Ernst, Emina Torlak
Generalized data structure synthesis. ICSE (2018)
Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, Xi Wang
Nickel: A Framework for Design and Verification of Information Flow Control Systems. OSDI (2018)
James Bornholt, Emina Torlak
Synthesizing memory models from framework sketches and Litmus tests. PLDI (2017)
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock
SpaceSearch: a library for building and verifying solver-aided tools. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, Xi Wang
Hyperkernel: Push-Button Verification of an OS Kernel. SOSP (2017)
Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak
Refinement Types for Ruby. CoRR (2017)
Eric Butler, Emina Torlak, Zoran Popovic
Synthesizing interpretable strategies for solving puzzle games. FDG (2017)
Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, Xi Wang
Push-Button Verification of File Systems via Crash Refinement. OSDI (2016)
Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock
Scalable verification of border gateway protocol configurations with an SMT solver. OOPSLA (2016)
Pavel Panchekha, Emina Torlak
Automated reasoning for web page layout. OOPSLA (2016)
James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze
Optimizing synthesis with metasketches. POPL (2016)
James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, Xi Wang
Specifying and Checking File System Crash-Consistency Models. ASPLOS (2016)
Eric Butler, Emina Torlak, Zoran Popovic
A Framework for Parameterized Design of Rule Systems Applied to Algebra. ITS (2016)
Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, Jonathan Jacky
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. CAV (2) (2016)
Calvin Loncaric, Emina Torlak, Michael D. Ernst
Fast synthesis of fast collections. PLDI (2016)
Rohin Shah, Emina Torlak, Rastislav Bodík
SIMPL: A DSL for Automatic Specialization of Inference Algorithms. CoRR (2016)
Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, Xi Wang
Toward a Dependability Case Language and Workflow for a Radiation Therapy System. SNAPL (2015)
John Toman, Stuart Pernsteiner, Emina Torlak
Crust: A Bounded Verifier for Rust (N). ASE (2015)
Shaon Barman, Rastislav Bodík, Satish Chandra, Emina Torlak, Arka Aloke Bhattacharya, David E. Culler
Toward tool support for interactive synthesis. Onward! (2015)
Emina Torlak, Rastislav Bodík
A lightweight symbolic virtual machine for solver-aided host languages. PLDI (2014)
Vijayaraghavan Murali, Nishant Sinha, Emina Torlak, Satish Chandra
What Gives? A Hybrid Algorithm for Error Trace Explanation. VSTTE (2014)
Emina Torlak, Rastislav Bodík
Growing solver-aided languages with rosette. Onward! (2013)
Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa
Syntax-guided synthesis. FMCAD (2013)
Emina Torlak, Mana Taghdiri, Greg Dennis, Joseph P. Near
Applications and extensions of Alloy: past, present and future. Math. Struct. Comput. Sci. 23 (4) (2013)
Emina Torlak
Scalable test data generation from multidimensional models. SIGSOFT FSE (2012)
Rastislav Bodík, Emina Torlak
Synthesizing Programs with Constraint Solvers. CAV (2012)
Satish Chandra, Emina Torlak, Shaon Barman, Rastislav Bodík
Angelic debugging. ICSE (2011)
Emina Torlak, Satish Chandra
Effective interprocedural resource leak detection. ICSE (1) (2010)
Max Schäfer, Julian Dolby, Manu Sridharan, Emina Torlak, Frank Tip
Correct Refactoring of Concurrent Java Code. ECOOP (2010)
Emina Torlak, Mandana Vaziri, Julian Dolby
MemSAT: checking axiomatic specifications of memory models. PLDI (2010)
Emina Torlak, Felix Sheng-Ho Chang, Daniel Jackson
Finding Minimal Unsatisfiable Cores of Declarative Specifications. FM (2008)
Blaise Gassend, Marten van Dijk, Dwaine E. Clarke, Emina Torlak, Srinivas Devadas, Pim Tuyls
Controlled physical random functions and applications. ACM Trans. Inf. Syst. Secur. 10 (4) (2008)
Emina Torlak, Daniel Jackson
Kodkod: A Relational Model Finder. TACAS (2007)
Emina Torlak, Marten van Dijk, Blaise Gassend, Daniel Jackson, Srinivas Devadas
Knowledge Flow Analysis for Security Protocols CoRR (2006)
Marten van Dijk, Emina Torlak, Blaise Gassend, Srinivas Devadas
A Generalized Two-Phase Analysis of Knowledge Flows in Security Protocols CoRR (2006)
Jonathan Edwards, Daniel Jackson, Emina Torlak
A type system for object models. SIGSOFT FSE (2004)
Jonathan Edwards, Daniel Jackson, Emina Torlak, Vincent Yeung
Faster constraint solving with subtypes. ISSTA (2004)

Emina Torlak.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Emina Torlak