Emina Torlak

Conference Papers

• [1] Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. Operating Systems Design and Implementation (OSDI), 2020. (DOI, PDF)
• [2] Yu Feng, Emina Torlak, and Rastislav Bodik. Summary-Based Symbolic Evaluation for Smart Contracts. Automated Software Engineering (ASE), 2020. Distinguished Paper Award. (PDF)
• [3] Jacob Van Geffen, Luke Nelson, Isil Dillig, Xi Wang, and Emina Torlak. Synthesizing JIT Compilers for In-Kernel DSLs. Computer Aided Verification (CAV), 2020. (DOI, PDF)
• [4] Sorawee Porncharoenwase, James Bornholt, and Emina Torlak. Fixing Code That Explodes Under Symbolic Evaluation. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2020. (DOI, PDF, Web)
• [5] Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. Symposium on Operating Systems Principles (SOSP), 2019. Best Paper and Distinguished Artifact Awards. (DOI, PDF, Web)
• [6] Phitchaya Mangpo Phothilimthana, Archibald Samuel Elliott, An Wang, Abhinav Jangda, Bastian Hagedorn, Henrik Barthels, Samuel J. Kaufman, Vinod Grover, Emina Torlak, and Rastislav Bodik. Swizzle Inventor: Data Movement Synthesis for GPU Kernels. Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2019. (DOI, PDF)
• [7] James Bornholt and Emina Torlak. Finding Code That Explodes Under Symbolic Evaluation. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2018. Distinguished Artifact Award. (DOI, PDF, Web)
• [8] Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. Nickel: A Framework for Design and Verification of Information Flow Control Systems. Operating Systems Design and Implementation (OSDI), 2018. (DOI, PDF, Web)
• [9] Calvin Loncaric, Michael D. Ernst, and Emina Torlak. Generalized Data Structure Synthesis. International Conference on Software Engineering (ICSE), 2018. Distinguished Paper Award. (DOI, PDF, Web)
• [10] Eric Butler, Emina Torlak, and Zoran Popovic. A Framework for Computer-Aided Design of Educational Domain Models. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2018. (DOI, PDF)
• [11] Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeff Foster, and Emina Torlak. Refinement Types for Ruby. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2018. (DOI, PDF)
• [12] Stephen Chang, Alex Knauth, and Emina Torlak. Symbolic Types for Lenient Symbolic Execution. Principles of Programming Languages (POPL), 2018. (DOI, PDF, Web)
• [13] Jonathan Jacky, Stefani Banerian, Michael D. Ernst, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, and Emina Torlak. Automatic Formal Verification for EPICS. International Conference on Accelerator and Large Experimental Control Systems (ICALEPCS), 2017. (DOI, PDF, Web)
• [14] Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-Button Verification of an OS Kernel. Symposium on Operating Systems Principles (SOSP), 2017. (DOI, PDF, Web)
• [15] Eric Butler, Emina Torlak, and Zoran Popovic. Synthesizing Interpretable Strategies for Solving Puzzle Games. Foundations of Digital Games (FDG), 2017. (DOI, PDF, Web)
• [16] James Bornholt and Emina Torlak. Synthesizing Memory Models from Framework Sketches and Litmus Tests. Programming Language Design and Implementation (PLDI), 2017. (DOI, PDF, Web)
• [17] Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock. SpaceSearch: A Library for Building and Verifying Solver-Aided Tools. International Conference on Functional Programming (ICFP), 2017. (DOI, PDF, Web)
• [18] Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-Button Verification of File Systems via Crash Refinement. Operating Systems Design and Implementation (OSDI), 2016. Best Paper Award. (DOI, PDF, Web)
• [19] Pavel Panchekha and Emina Torlak. Automated Reasoning for Web Page Layout. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016. (DOI, PDF, Web)
• [20] Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016. (DOI, PDF, Web)
• [21] Stuart Pernsteiner, Calvin Loncaric, Emina Torlak, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Jonathan Jacky. Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. Computer-Aided Verification (CAV), 2016. (DOI, PDF, Web)
• [22] Eric Butler, Emina Torlak, and Zoran Popovic. A Framework for Parameterized Design of Rule Systems Applied to Algebra. Intelligent Tutoring Systems (ITS), 2016. (DOI, PDF)
• [23] Calvin Loncaric, Emina Torlak, and Michael D. Ernst. Fast synthesis of fast collections. Programming Language Design and Implementation (PLDI), 2016. (DOI, PDF, Web)
• [24] James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Specifying and Checking File System Crash-Consistency Models. Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2016. (DOI, PDF, Web)
• [25] James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. Principles of Programming Languages (POPL), 2016. (DOI, PDF, Web)
• [26] Shaon Barman, Rastislav Bodik, Satish Chandra, Emina Torlak, Arka Bhattacharya, and David Culler. Toward Tool Support for Interactive Synthesis. New Ideas, New Paradigms, and Reflections on Programming & Software (Onward!), 2015. (DOI, PDF)
• [27] John Toman, Stuart Pernsteiner, and Emina Torlak. CRust: A Bounded Verifier for Rust. Automated Software Engineering (ASE), 2015. (DOI, PDF, Web)
• [28] Michael Ernst, Dan Grossman, Jon Jacky, Calvin Loncaric, Stuart Pernsteiner, Zachary Tatlock, Emina Torlak, and Xi Wang. Toward a Dependability Case Language and Workflow for a Radiation Therapy System. Summit on Advances in Programming Languages (SNAPL), 2015. (DOI, PDF, Web)
• [29] Emina Torlak and Rastislav Bodik. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. Programming Language Design and Implementation (PLDI), 2014. (DOI, PDF, Web)
• [30] Vijayaraghavan Murali, Nishant Sinha, Emina Torlak, and Satish Chandra. What Gives?: A Hybrid Algorithm for Error Trace Explanation. Verified Software: Theories, Tools and Experiments (VSTTE), 2014. (DOI, PDF)
• [31] Emina Torlak and Rastislav Bodik. Growing Solver-Aided Languages with Rosette. New Ideas, New Paradigms, and Reflections on Programming & Software (Onward!), 2013. (DOI, PDF, Web)
• [32] Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-Guided Synthesis. Formal Methods in Computer-Aided Design (FMCAD), 2013. (PDF)
• [33] Rastislav Bodik and Emina Torlak. Synthesizing Programs with Constraint Solvers (Invited Tutorial). Computer Aided Verification (CAV), 2012.
• [34] Emina Torlak. Scalable test data generation from multidimensional models. Foundations of Software Engineering (FSE), 2012. Distinguished Paper Award. (DOI, PDF)
• [35] Satish Chandra, Emina Torlak, Shaon Barman, and Rastislav Bodik. Angelic Debugging. International Conference on Software Engineering (ICSE), 2011. (DOI, PDF)
• [36] Max Schaefer, Julian Dolby, Manu Sridharan, Emina Torlak, and Frank Tip. Correct Refactoring of Concurrent Java Code. European Conference on Object-Oriented Programming (ECOOP), 2010. (DOI, PDF)
• [37] Emina Torlak, Mandana Vaziri, and Julian Dolby. MemSAT: Checking Axiomatic Specifications of Memory Models. Programming Language Design and Implementation (PLDI), 2010. (DOI, PDF, Web)
• [38] Emina Torlak, and Satish Chandra. Effective interprocedural resource leak detection. International Conference on Software Engineering (ICSE), 2010. (DOI, PDF)
• [39] Emina Torlak, Felix Sheng-Ho Chang, and Daniel Jackson. Finding Minimal Unsatisfiable Cores of Declarative Specifications. Formal Methods (FM), 2008. (DOI, PDF, Web)
• [40] Emina Torlak and Daniel Jackson. Kodkod: A Relational Model Finder. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007. (DOI, PDF, Web)
• [41] Jonathan Edwards, Daniel Jackson, Emina Torlak, and Vincent Yeung. Faster constraint solving with subtypes. International Symposium on Software Testing and Analysis (ISSTA), 2004. (DOI, PDF, Web)
• [42] Jonathan Edwards, Daniel Jackson, and Emina Torlak. A type system for object models. Foundations of Software Engineering (FSE), 2004. (DOI, PDF, Web)

Journal Papers

• [43] Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Noninterference specifications for secure systems. ACM SIGOPS Operating Systems Review, 2020. (DOI, PDF)
• [44] Rajeev Alur, Rastislav Bodik, 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, and Abhishek Udupa. Syntax-Guided Synthesis. Dependable Software Systems Engineering, 2015. (DOI, PDF)
• [45] Emina Torlak, Mana Taghdiri, Greg Dennis, and Joseph Near. Applications and Extensions of Alloy: Past, Present, and Future. (Invited Paper). Mathematical Structures in Computer Science (MSCS), 2013. (DOI, PDF)
• [46] Blaise Gassend, Marten Van Dijk, Dwaine Clarke, Emina Torlak, Srinivas Devadas, and Pim Tuyls. Controlled physical random functions and applications. ACM Transactions on Information and System Security (TISSEC), 2008. (DOI, PDF)

Workshop Papers

• [47] Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. Formal Semantics and Automated Verification for the Border Gateway Protocol. ACM SIGCOMM Workshop on Networking and Programming Languages (NetPL), 2016. (PDF, Web)
• [48] James Bornholt and Emina Torlak. Scaling program synthesis by exploiting existing code. Machine Learning for Programming Languages Workshop (ML4PL), 2015. (PDF)
• [49] James Bornholt, Emina Torlak, Luis Ceze, and Dan Grossman. Approximate Program Synthesis. Workshop on Approximate Computing Across the Stack (WAX), 2015. (PDF)
• [50] Emina Torlak and Greg Dennis. Kodkod for Alloy Users. Alloy Workshop, 2006. (PDF, Web)

Technical Reports

• [51] Eric Butler, Emina Torlak, and Zoran Popovic. Synthesizing Optimal Domain Models for Educational Applications. University of Washington Computer Science & Engineering, 2017. (DOI)
• [52] Konstantin Weitz, Dough Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. Bagpipe: Verified BGP Configuration Checking. University of Washington Computer Science & Engineering, 2016. (DOI, Web)
• [53] Emina Torlak. Scalable Test Data Generation from Multidimensional Models. University of California, Berkeley, 2012. (DOI)
• [54] Shaon Barman, Ras Bodik, Satish Chandra, and Emina Torlak. Discovering Algorithms in Angelic Programs. IBM Research, 2010.
• [55] Emina Torlak and Daniel Jackson. The Design of a Relational Engine. Massachusetts Institute of Technology, 2006. (DOI)
• [56] Marten van Dijk, Emina Torlak, Blaise Gassend, and Srinivas Devadas. A Generalized Two-Phase Analysis of Knowledge Flows in Security Protocols. arXiv.org, 2006. (DOI)
• [57] Emina Torlak, Marten van Dijk, Blaise Gassend, Daniel Jackson, and Srinivas Devadas. Knowledge Flow Analysis for Security Protocols. arXiv.org, 2006. (DOI)

Theses

• [58] Emina Torlak. A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications. Massachusetts Institute of Technology, 2009. (DOI, PDF, Web)
• [59] Emina Torlak. Subtyping in Alloy. Massachusetts Institute of Technology, 2004. (PDF, Web)