Emina Torlak

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

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization.

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

Proc. ACM Program. Lang., 2024

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

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

CoRR, 2024

How We Built Cedar: A Verification-Guided Approach.

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

Proceedings of the Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, 2024

2023

A Pretty Expressive Printer.

Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak

Proc. ACM Program. Lang., October, 2023

A Pretty Expressive Printer (with Appendices).

Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak

CoRR, 2023

Synthesis-Aided Crash Consistency for Storage Systems.

Jacob Van Geffen, Xi Wang, Emina Torlak, James Bornholt

Proceedings of the 37th European Conference on Object-Oriented Programming, 2023

2022

A formal foundation for symbolic evaluation with merging.

Sorawee Porncharoenwase, Luke Nelson, Xi Wang, Emina Torlak

Proc. ACM Program. Lang., 2022

Testing Dafny (experience paper).

Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamaric, Neha Rungta, Emina Torlak

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.

Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, Xi Wang

ACM SIGOPS Oper. Syst. Rev., 2020

Fixing Code that Explodes Under Symbolic Evaluation.

Sorawee Porncharoenwase, James Bornholt, Emina Torlak

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.

Luke Nelson, Jacob Van Geffen, Emina Torlak, Xi Wang

Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation, 2020

Summary-Based Symbolic Evaluation for Smart Contracts.

Yu Feng, Emina Torlak, Rastislav Bodík

Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

Synthesizing JIT Compilers for In-Kernel DSLs.

Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, Emina Torlak

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Precise Attack Synthesis for Smart Contracts.

Yu Feng, Emina Torlak, Rastislav Bodík

CoRR, 2019

Scaling symbolic evaluation for automated verification of systems code with Serval.

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang

Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

Swizzle Inventor: Data Movement Synthesis for GPU Kernels.

Phitchaya Mangpo Phothilimthana, Archibald Samuel Elliott, An Wang, Abhinav Jangda, Bastian Hagedorn, Henrik Barthels, Samuel J. Kaufman, Vinod Grover, Emina Torlak, Rastislav Bodík

Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, 2019

2018

Symbolic types for lenient symbolic execution.

Stephen Chang, Alex Knauth, Emina Torlak

Proc. ACM Program. Lang., 2018

Finding code that explodes under symbolic evaluation.

James Bornholt, Emina Torlak

Proc. ACM Program. Lang., 2018

Refinement Types for Ruby.

Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

A Framework for Computer-Aided Design of Educational Domain Models.

Eric Butler, Emina Torlak, Zoran Popovic

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Nickel: A Framework for Design and Verification of Information Flow Control Systems.

Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, Xi Wang

Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation, 2018

Generalized data structure synthesis.

Calvin Loncaric, Michael D. Ernst, Emina Torlak

Proceedings of the 40th International Conference on Software Engineering, 2018

2017

SpaceSearch: a library for building and verifying solver-aided tools.

Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock

Proc. ACM Program. Lang., 2017

Hyperkernel: Push-Button Verification of an OS Kernel.

Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, Xi Wang

Proceedings of the 26th Symposium on Operating Systems Principles, 2017

Synthesizing memory models from framework sketches and Litmus tests.

James Bornholt, Emina Torlak

Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017

Synthesizing interpretable strategies for solving puzzle games.

Eric Butler, Emina Torlak, Zoran Popovic

Proceedings of the International Conference on the Foundations of Digital Games, 2017

2016

SIMPL: A DSL for Automatic Specialization of Inference Algorithms.

Rohin Shah, Emina Torlak, Rastislav Bodík

CoRR, 2016

Optimizing synthesis with metasketches.

James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Fast synthesis of fast collections.

Calvin Loncaric, Emina Torlak, Michael D. Ernst

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

Push-Button Verification of File Systems via Crash Refinement.

Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, Xi Wang

Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, 2016

Scalable verification of border gateway protocol configurations with an SMT solver.

Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock

Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

Automated reasoning for web page layout.

Pavel Panchekha, Emina Torlak

Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

A Framework for Parameterized Design of Rule Systems Applied to Algebra.

Eric Butler, Emina Torlak, Zoran Popovic

Proceedings of the Intelligent Tutoring Systems - 13th International Conference, 2016

Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers.

Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, Jonathan Jacky

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

Specifying and Checking File System Crash-Consistency Models.

James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, Xi Wang

Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, 2016

2015

Syntax-Guided Synthesis.

Rajeev Alur, Rastislav Bodík, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa

Proceedings of the Dependable Software Systems Engineering, 2015

Toward a Dependability Case Language and Workflow for a Radiation Therapy System.

Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, Xi Wang

Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Toward tool support for interactive synthesis.

Shaon Barman, Rastislav Bodík, Satish Chandra, Emina Torlak, Arka Aloke Bhattacharya, David E. Culler

Proceedings of the 2015 ACM International Symposium on New Ideas, 2015

Crust: A Bounded Verifier for Rust (N).

John Toman, Stuart Pernsteiner, Emina Torlak

Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, 2015

2014

What Gives? A Hybrid Algorithm for Error Trace Explanation.

Vijayaraghavan Murali, Nishant Sinha, Emina Torlak, Satish Chandra

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

A lightweight symbolic virtual machine for solver-aided host languages.

Emina Torlak, Rastislav Bodík

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2014

2013

Applications and extensions of Alloy: past, present and future.

Emina Torlak, Mana Taghdiri, Greg Dennis, Joseph P. Near

Math. Struct. Comput. Sci., 2013

Growing solver-aided languages with rosette.

Emina Torlak, Rastislav Bodík

Proceedings of the ACM Symposium on New Ideas in Programming and Reflections on Software, 2013

Syntax-guided synthesis.

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

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

Scalable test data generation from multidimensional models.

Emina Torlak

Proceedings of the 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), 2012

Synthesizing Programs with Constraint Solvers.

Rastislav Bodík, Emina Torlak

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Angelic debugging.

Satish Chandra, Emina Torlak, Shaon Barman, Rastislav Bodík

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

2010

MemSAT: checking axiomatic specifications of memory models.

Emina Torlak, Mandana Vaziri, Julian Dolby

Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010

Effective interprocedural resource leak detection.

Emina Torlak, Satish Chandra

Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

Correct Refactoring of Concurrent Java Code.

Max Schäfer, Julian Dolby, Manu Sridharan, Emina Torlak, Frank Tip

Proceedings of the ECOOP 2010, 2010

2009

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

Emina Torlak

PhD thesis, 2009

2008

Controlled physical random functions and applications.

Blaise Gassend, Marten van Dijk, Dwaine E. Clarke, Emina Torlak, Srinivas Devadas, Pim Tuyls

ACM Trans. Inf. Syst. Secur., 2008

Finding Minimal Unsatisfiable Cores of Declarative Specifications.

Emina Torlak, Felix Sheng-Ho Chang, Daniel Jackson

Proceedings of the FM 2008: Formal Methods, 2008

2007

Kodkod: A Relational Model Finder.

Emina Torlak, Daniel Jackson

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

2006

Knowledge Flow Analysis for Security Protocols

Emina Torlak, Marten van Dijk, Blaise Gassend, Daniel Jackson, Srinivas Devadas

CoRR, 2006

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

Marten van Dijk, Emina Torlak, Blaise Gassend, Srinivas Devadas

CoRR, 2006

2004

A type system for object models.

Jonathan Edwards, Daniel Jackson, Emina Torlak

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.

Jonathan Edwards, Daniel Jackson, Emina Torlak, Vincent Yeung

Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, 2004