Emina Torlak

Research

My research aims to help people create better software more easily. As part of this agenda, I develop new languages and tools for computer-aided design, verification, and synthesis of software. My collaborators and I apply these techniques to all kinds of systems, from radiotherapy machines to automated algebra tutors. A lot of our work is based on Rosette, a new language that makes it easy to create efficient tools for program verification, synthesis, and more.

News  
Sep 18 Gave the keynote at RacketCon’16.
Jul 22 Gave the Junior DN Prize Lecture at ECOOP’16.
Mar 25 Released Rosette 2.0: new theories, better performance!
Feb 28 Received a Sloan Research Fellowship.
Jan 20 Won the AITO Dahl-Nygaard Junior Prize.

All Publications

Recent Publications DBLP Google Scholar

Conference and Journal Papers

  • [1] 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)
  • [2] Pavel Panchekha and Emina Torlak. Automated Reasoning for Web Page Layout. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016. (DOI, PDF, Web)
  • [3] 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)
  • [4] 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)
  • [5] 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)
  • [6] Calvin Loncaric, Emina Torlak, and Michael D. Ernst. Fast synthesis of fast collections. Programming Language Design and Implementation (PLDI), 2016. (DOI, PDF, Web)
  • [7] 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)
  • [8] James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. Principles of Programming Languages (POPL), 2016. (DOI, PDF, Web)
  • [9] 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 and Software (Onward!), 2015. (DOI, PDF)
  • [10] John Toman, Stuart Pernsteiner, and Emina Torlak. CRust: A Bounded Verifier for Rust. Automated Software Engineering (ASE), 2015. (PDF, Web)
  • [11] 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)
  • [12] 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)
  • [13] 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)
  • [14] 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)
  • [15] Emina Torlak and Rastislav Bodik. Growing Solver-Aided Languages with Rosette. New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), 2013. (DOI, PDF, Web)
  • [16] 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)
  • [17] 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)
  • [18] Rastislav Bodik and Emina Torlak. Synthesizing Programs with Constraint Solvers (Invited Tutorial). Computer Aided Verification (CAV), 2012.
  • [19] Emina Torlak. Scalable test data generation from multidimensional models. Foundations of Software Engineering (FSE), 2012. Distinguished Paper Award. (DOI, PDF)
  • [20] Satish Chandra, Emina Torlak, Shaon Barman, and Rastislav Bodik. Angelic Debugging. International Conference on Software Engineering (ICSE), 2011. (DOI, PDF)
  • [21] 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)
  • [22] Emina Torlak, Mandana Vaziri, and Julian Dolby. MemSAT: Checking Axiomatic Specifications of Memory Models. Programming Language Design and Implementation (PLDI), 2010. (DOI, PDF, Web)
  • [23] Emina Torlak and Satish Chandra. Effective interprocedural resource leak detection. International Conference on Software Engineering (ICSE), 2010. (DOI, PDF)
  • [24] Emina Torlak, Felix Sheng-Ho Chang, and Daniel Jackson. Finding Minimal Unsatisfiable Cores of Declarative Specifications. Formal Methods (FM), 2008. (DOI, PDF, Web)
  • [25] 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)
  • [26] 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)
  • [27] 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)
  • [28] Jonathan Edwards, Daniel Jackson, and Emina Torlak. A type system for object models. Foundations of Software Engineering (FSE), 2004. (DOI, PDF, Web)

Workshop Papers

  • [1] 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)
  • [2] James Bornholt and Emina Torlak. Scaling program synthesis by exploiting existing code. Machine Learning for Programming Languages Workshop (ML4PL), 2015. (PDF)
  • [3] James Bornholt, Emina Torlak, Luis Ceze, and Dan Grossman. Approximate Program Synthesis. Workshop on Approximate Computing Across the Stack (WAX), 2015. (PDF)
  • [4] Emina Torlak and Greg Dennis. Kodkod for Alloy Users. Alloy Workshop, 2006. (PDF, Web)

Tech Reports and Theses

  • [1] Konstantin Weitz, Dough Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, and Zachary Tatlock. Bagpipe: Verified BGP Configuration Checking. University of Washington Computer Science and Engineering Technical Report, 2016. (UW-CSE-16-01-01, Web)
  • [2] Emina Torlak. Scalable Test Data Generation from Multidimensional Models. University of California, Berkeley Technical Report, 2012. (UCB/EECS-2012-177)
  • [3] Shaon Barman, Ras Bodik, Satish Chandra, and Emina Torlak. Discovering Algorithms in Angelic Programs. IBM Research Technical Report, 2010. (RC25023)
  • [4] Emina Torlak and Daniel Jackson. The Design of a Relational Engine. Massachusetts Institute of Technology Technical Report, 2006. (MIT-CSAIL-TR-2006-068)
  • [5] Marten van Dijk, Emina Torlak, Blaise Gassend, and Srinivas Devadas. A Generalized Two-Phase Analysis of Knowledge Flows in Security Protocols. arXiv.org Technical Report, 2006. (arXiv:cs/0605097v1)
  • [6] Emina Torlak, Marten van Dijk, Blaise Gassend, Daniel Jackson, and Srinivas Devadas. Knowledge Flow Analysis for Security Protocols. arXiv.org Technical Report, 2006. (arXiv:cs/0605109v1)
  • [7] Emina Torlak. A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications. Massachusetts Institute of Technology Ph.D. Thesis, 2009. (DOI, PDF, Web)
  • [8] Emina Torlak. Subtyping in Alloy. Massachusetts Institute of Technology Masters Thesis, 2004. (PDF, Web)