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.
Recent Publications
- [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.
- [2] Pavel Panchekha and Emina Torlak. Automated Reasoning for Web Page Layout. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016. (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. (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)
