Emina Torlak

63 papers A* 19A 7B 6C 1Journal 17Unranked 10
YearRankTypeTitle / Venue / Authors
2025 A* conf
Formally Verified Cloud-Scale Authorization.
ICSE
Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clément Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas G. Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Tae Joon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan
2024 J jnl
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version).
CoRR
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
2024 J jnl
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization.
Proc. ACM Program. Lang.
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
2024 — conf
How We Built Cedar: A Verification-Guided Approach.
SIGSOFT FSE Companion
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
2024 J jnl
How We Built Cedar: A Verification-Guided Approach.
CoRR
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
2023 J jnl
A Pretty Expressive Printer (with Appendices).
CoRR
Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak
2023 J jnl
A Pretty Expressive Printer.
Proc. ACM Program. Lang.
Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak
2023 A conf
Synthesis-Aided Crash Consistency for Storage Systems.
ECOOP
Jacob Van Geffen, Xi Wang, Emina Torlak, James Bornholt
2022 J jnl
A formal foundation for symbolic evaluation with merging.
Proc. ACM Program. Lang.
Sorawee Porncharoenwase, Luke Nelson, Xi Wang, Emina Torlak
2022 A conf
Testing Dafny (experience paper).
ISSTA
Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamaric, Neha Rungta, Emina Torlak
2020 B conf
Fixing Code that Explodes Under Symbolic Evaluation.
VMCAI
Sorawee Porncharoenwase, James Bornholt, Emina Torlak
2020 J jnl
Noninterference specifications for secure systems.
ACM SIGOPS Oper. Syst. Rev.
Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, Xi Wang
2020 A* ed.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020
PLDI
Alastair F. Donaldson, Emina Torlak
2020 A* conf
Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel.
OSDI
Luke Nelson, Jacob Van Geffen, Emina Torlak, Xi Wang
2020 A* conf
Summary-Based Symbolic Evaluation for Smart Contracts.
ASE
Yu Feng, Emina Torlak, Rastislav Bodík
2020 — conf
Synthesizing JIT Compilers for In-Kernel DSLs.
CAV (2)
Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, Emina Torlak
2019 J jnl
Precise Attack Synthesis for Smart Contracts.
CoRR
Yu Feng, Emina Torlak, Rastislav Bodík
2019 A* conf
Scaling symbolic evaluation for automated verification of systems code with Serval.
SOSP
Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang
2019 A* conf
Swizzle Inventor: Data Movement Synthesis for GPU Kernels.
ASPLOS
Phitchaya Mangpo Phothilimthana, Archibald Samuel Elliott, An Wang, Abhinav Jangda, Bastian Hagedorn, Henrik Barthels, Samuel J. Kaufman, Vinod Grover, Emina Torlak, Rastislav Bodík
2018 B conf
A Framework for Computer-Aided Design of Educational Domain Models.
VMCAI
Eric Butler, Emina Torlak, Zoran Popovic
2018 J jnl
Finding code that explodes under symbolic evaluation.
Proc. ACM Program. Lang.
James Bornholt, Emina Torlak
2018 A* conf
Generalized data structure synthesis.
ICSE
Calvin Loncaric, Michael D. Ernst, Emina Torlak
2018 A* conf
Nickel: A Framework for Design and Verification of Information Flow Control Systems.
OSDI
Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, Xi Wang
2018 B conf
Refinement Types for Ruby.
VMCAI
Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak
2018 J jnl
Symbolic types for lenient symbolic execution.
Proc. ACM Program. Lang.
Stephen Chang, Alex Knauth, Emina Torlak
2017 A* conf
Hyperkernel: Push-Button Verification of an OS Kernel.
SOSP
Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, Xi Wang
2017 — ed.
Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2017, Vancouver, BC, Canada, October 23 - 27, 2017
Onward!
Emina Torlak, Tijs van der Storm, Robert Biddle
2017 J jnl
Refinement Types for Ruby.
CoRR
Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak
2017 J jnl
SpaceSearch: a library for building and verifying solver-aided tools.
Proc. ACM Program. Lang.
Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock
2017 C conf
Synthesizing interpretable strategies for solving puzzle games.
FDG
Eric Butler, Emina Torlak, Zoran Popovic
2017 A* conf
Synthesizing memory models from framework sketches and Litmus tests.
PLDI
James Bornholt, Emina Torlak
2016 B conf
A Framework for Parameterized Design of Rule Systems Applied to Algebra.
ITS
Eric Butler, Emina Torlak, Zoran Popovic
2016 A conf
Automated reasoning for web page layout.
OOPSLA
Pavel Panchekha, Emina Torlak
2016 A* conf
Fast synthesis of fast collections.
PLDI
Calvin Loncaric, Emina Torlak, Michael D. Ernst
2016 — conf
Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers.
CAV (2)
Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, Jonathan Jacky
2016 A* conf
Optimizing synthesis with metasketches.
POPL
James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze
2016 A* conf
Push-Button Verification of File Systems via Crash Refinement.
OSDI
Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, Xi Wang
2016 J jnl
SIMPL: A DSL for Automatic Specialization of Inference Algorithms.
CoRR
Rohin Shah, Emina Torlak, Rastislav Bodík
2016 A conf
Scalable verification of border gateway protocol configurations with an SMT solver.
OOPSLA
Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock
2016 A* conf
Specifying and Checking File System Crash-Consistency Models.
ASPLOS
James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, Xi Wang
2015 A* conf
Crust: A Bounded Verifier for Rust (N).
ASE
John Toman, Stuart Pernsteiner, Emina Torlak
2015 — ch.
Syntax-Guided Synthesis.
Dependable Software Systems Engineering
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
2015 — conf
Toward a Dependability Case Language and Workflow for a Radiation Therapy System.
SNAPL
Michael D. Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, Xi Wang
2015 — conf
Toward tool support for interactive synthesis.
Onward!
Shaon Barman, Rastislav Bodík, Satish Chandra, Emina Torlak, Arka Aloke Bhattacharya, David E. Culler
2014 A* conf
A lightweight symbolic virtual machine for solver-aided host languages.
PLDI
Emina Torlak, Rastislav Bodík
2014 — conf
What Gives? A Hybrid Algorithm for Error Trace Explanation.
VSTTE
Vijayaraghavan Murali, Nishant Sinha, Emina Torlak, Satish Chandra
2013 J jnl
Applications and extensions of Alloy: past, present and future.
Math. Struct. Comput. Sci.
Emina Torlak, Mana Taghdiri, Greg Dennis, Joseph P. Near
2013 — conf
Growing solver-aided languages with rosette.
Onward!
Emina Torlak, Rastislav Bodík
2013 B conf
Syntax-guided synthesis.
FMCAD
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
2012 — conf
Scalable test data generation from multidimensional models.
SIGSOFT FSE
Emina Torlak
2012 A* conf
Synthesizing Programs with Constraint Solvers.
CAV
Rastislav Bodík, Emina Torlak
2011 A* conf
Angelic debugging.
ICSE
Satish Chandra, Emina Torlak, Shaon Barman, Rastislav Bodík
2010 A conf
Correct Refactoring of Concurrent Java Code.
ECOOP
Max Schäfer, Julian Dolby, Manu Sridharan, Emina Torlak, Frank Tip
2010 — conf
Effective interprocedural resource leak detection.
ICSE (1)
Emina Torlak, Satish Chandra
2010 A* conf
MemSAT: checking axiomatic specifications of memory models.
PLDI
Emina Torlak, Mandana Vaziri, Julian Dolby
2009 — —
A constraint solver for software engineering: finding models and cores of large relational specifications.
Emina Torlak
2008 J jnl
Controlled physical random functions and applications.
ACM Trans. Inf. Syst. Secur.
Blaise Gassend, Marten van Dijk, Dwaine E. Clarke, Emina Torlak, Srinivas Devadas, Pim Tuyls
2008 B conf
Finding Minimal Unsatisfiable Cores of Declarative Specifications.
FM
Emina Torlak, Felix Sheng-Ho Chang, Daniel Jackson
2007 A conf
Kodkod: A Relational Model Finder.
TACAS
Emina Torlak, Daniel Jackson
2006 J jnl
A Generalized Two-Phase Analysis of Knowledge Flows in Security Protocols
CoRR
Marten van Dijk, Emina Torlak, Blaise Gassend, Srinivas Devadas
2006 J jnl
Knowledge Flow Analysis for Security Protocols
CoRR
Emina Torlak, Marten van Dijk, Blaise Gassend, Daniel Jackson, Srinivas Devadas
2004 — conf
A type system for object models.
SIGSOFT FSE
Jonathan Edwards, Daniel Jackson, Emina Torlak
2004 A conf
Faster constraint solving with subtypes.
ISSTA
Jonathan Edwards, Daniel Jackson, Emina Torlak, Vincent Yeung