Faster constraint solving with subtypes. - Jonathan Edwards; Daniel Jackson 001; Emina Torlak; Vincent Yeung (ISSTA, 2004)

A type system for object models. - Jonathan Edwards; Daniel Jackson 001; Emina Torlak (SIGSOFT FSE, 2004)

A Generalized Two-Phase Analysis of Knowledge Flows in Security Protocols - Marten van Dijk; Emina Torlak; Blaise Gassend; Srinivas Devadas (CoRR, 2006)

Knowledge Flow Analysis for Security Protocols - Emina Torlak; Marten van Dijk; Blaise Gassend; Daniel Jackson 001; Srinivas Devadas (CoRR, 2006)

Kodkod: A Relational Model Finder. - Emina Torlak; Daniel Jackson 001 (TACAS, 2007)

Finding Minimal Unsatisfiable Cores of Declarative Specifications. - Emina Torlak; Felix Sheng-Ho Chang; Daniel Jackson 001 (FM, 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)

A constraint solver for software engineering: finding models and cores of large relational specifications. - Emina Torlak (2009)

Correct Refactoring of Concurrent Java Code. - Max Schäfer; Julian Dolby; Manu Sridharan; Emina Torlak; Frank Tip (ECOOP, 2010)

Effective interprocedural resource leak detection. - Emina Torlak; Satish Chandra 001 (ICSE (1), 2010)

MemSAT: checking axiomatic specifications of memory models. - Emina Torlak; Mandana Vaziri; Julian Dolby (PLDI, 2010)

Angelic debugging. - Satish Chandra 001; Emina Torlak; Shaon Barman; Rastislav Bodík (ICSE, 2011)

Synthesizing Programs with Constraint Solvers. - Rastislav Bodík; Emina Torlak (CAV, 2012)

Scalable test data generation from multidimensional models. - Emina Torlak (SIGSOFT FSE, 2012)

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 (FMCAD, 2013)

Growing solver-aided languages with rosette. - Emina Torlak; Rastislav Bodík (Onward!, 2013)

Applications and extensions of Alloy: past, present and future. - Emina Torlak; Mana Taghdiri; Greg Dennis; Joseph P. Near (Math. Struct. Comput. Sci., 2013)

A lightweight symbolic virtual machine for solver-aided host languages. - Emina Torlak; Rastislav Bodík (PLDI, 2014)

What Gives? A Hybrid Algorithm for Error Trace Explanation. - Vijayaraghavan Murali; Nishant Sinha 001; Emina Torlak; Satish Chandra 001 (VSTTE, 2014)

Crust: A Bounded Verifier for Rust (N). - John Toman; Stuart Pernsteiner; Emina Torlak (ASE, 2015)

Toward tool support for interactive synthesis. - Shaon Barman; Rastislav Bodík; Satish Chandra 001; Emina Torlak; Arka Aloke Bhattacharya; David E. Culler (Onward!, 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 005 (SNAPL, 2015)

Syntax-Guided Synthesis. - Rajeev Alur; Rastislav Bodík; Eric Dallal; Dana Fisman; Pranav Garg 001; Garvit Juniwal; Hadas Kress-Gazit; P. Madhusudan; Milo M. K. Martin; Mukund Raghothaman; Shambwaditya Saha; Sanjit A. Seshia; et al. (Dependable Software Systems Engineering, 2015)

Specifying and Checking File System Crash-Consistency Models. - James Bornholt; Antoine Kaufmann; Jialin Li 001; Arvind Krishnamurthy; Emina Torlak; Xi Wang 005 (ASPLOS, 2016)

Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. - Stuart Pernsteiner; Calvin Loncaric; Emina Torlak; Zachary Tatlock; Xi Wang 005; Michael D. Ernst; Jonathan Jacky (CAV (2), 2016)

A Framework for Parameterized Design of Rule Systems Applied to Algebra. - Eric Butler; Emina Torlak; Zoran Popovic (ITS, 2016)

Automated reasoning for web page layout. - Pavel Panchekha; Emina Torlak (OOPSLA, 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 (OOPSLA, 2016)

Push-Button Verification of File Systems via Crash Refinement. - Helgi Sigurbjarnarson; James Bornholt; Emina Torlak; Xi Wang 005 (OSDI, 2016)

Fast synthesis of fast collections. - Calvin Loncaric; Emina Torlak; Michael D. Ernst (PLDI, 2016)

Optimizing synthesis with metasketches. - James Bornholt; Emina Torlak; Dan Grossman; Luis Ceze (POPL, 2016)

SIMPL: A DSL for Automatic Specialization of Inference Algorithms. - Rohin Shah; Emina Torlak; Rastislav Bodík (CoRR, 2016)

Synthesizing interpretable strategies for solving puzzle games. - Eric Butler; Emina Torlak; Zoran Popovic (FDG, 2017)

Synthesizing memory models from framework sketches and Litmus tests. - James Bornholt; Emina Torlak (PLDI, 2017)

Hyperkernel: Push-Button Verification of an OS Kernel. - Luke Nelson; Helgi Sigurbjarnarson; Kaiyuan Zhang 001; Dylan Johnson; James Bornholt; Emina Torlak; Xi Wang 005 (SOSP, 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)

Generalized data structure synthesis. - Calvin Loncaric; Michael D. Ernst; Emina Torlak (ICSE, 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 005 (OSDI, 2018)

A Framework for Computer-Aided Design of Educational Domain Models. - Eric Butler; Emina Torlak; Zoran Popovic (VMCAI, 2018)

Refinement Types for Ruby. - Milod Kazerounian; Niki Vazou; Austin Bourgerie; Jeffrey S. Foster; Emina Torlak (VMCAI, 2018)

Finding code that explodes under symbolic evaluation. - James Bornholt; Emina Torlak (Proc. ACM Program. Lang., 2018)

Symbolic types for lenient symbolic execution. - Stephen Chang 001; Alex Knauth; Emina Torlak (Proc. ACM Program. Lang., 2018)

Swizzle Inventor: Data Movement Synthesis for GPU Kernels. - Phitchaya Mangpo Phothilimthana; Archibald Samuel Elliott; An Wang 003; Abhinav Jangda; Bastian Hagedorn; Henrik Barthels; Samuel J. Kaufman; Vinod Grover; Emina Torlak; Rastislav Bodík (ASPLOS, 2019)

Scaling symbolic evaluation for automated verification of systems code with Serval. - Luke Nelson; James Bornholt; Ronghui Gu; Andrew Baumann; Emina Torlak; Xi Wang 005 (SOSP, 2019)

Precise Attack Synthesis for Smart Contracts. - Yu Feng 001; Emina Torlak; Rastislav Bodík (CoRR, 2019)

Synthesizing JIT Compilers for In-Kernel DSLs. - Jacob Van Geffen; Luke Nelson; Isil Dillig; Xi Wang 005; Emina Torlak (CAV (2), 2020)

Summary-Based Symbolic Evaluation for Smart Contracts. - Yu Feng 001; Emina Torlak; Rastislav Bodík (ASE, 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 005 (OSDI, 2020)

Fixing Code that Explodes Under Symbolic Evaluation. - Sorawee Porncharoenwase; James Bornholt; Emina Torlak (VMCAI, 2020)

Noninterference specifications for secure systems. - Luke Nelson; James Bornholt; Arvind Krishnamurthy; Emina Torlak; Xi Wang 005 (ACM SIGOPS Oper. Syst. Rev., 2020)

Testing Dafny (experience paper). - Ahmed Irfan; Sorawee Porncharoenwase; Zvonimir Rakamaric; Neha Rungta; Emina Torlak (ISSTA, 2022)

A formal foundation for symbolic evaluation with merging. - Sorawee Porncharoenwase; Luke Nelson; Xi Wang 005; Emina Torlak (Proc. ACM Program. Lang., 2022)

Synthesis-Aided Crash Consistency for Storage Systems. - Jacob Van Geffen; Xi Wang 005; Emina Torlak; James Bornholt (ECOOP, 2023)

A Pretty Expressive Printer (with Appendices). - Sorawee Porncharoenwase; Justin Pombrio; Emina Torlak (CoRR, 2023)

A Pretty Expressive Printer. - Sorawee Porncharoenwase; Justin Pombrio; Emina Torlak (Proc. ACM Program. Lang., 2023)

How We Built Cedar: A Verification-Guided Approach. - Craig Disselkoen; Aaron Eline; Shaobo He; Kyle Headley; Michael Hicks 001; Kesha Hietala; John H. Kastner; Anwar Mamat; Matt McCutchen; Neha Rungta; Bhakti Shah; Emina Torlak; et al. (SIGSOFT FSE Companion, 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 001; Kesha Hietala; Eleftherios Ioannidis; John H. Kastner; Anwar Mamat; Darin McAdams; Matt McCutchen; et al. (CoRR, 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 001; Kesha Hietala; Eleftherios Ioannidis; John H. Kastner; Anwar Mamat; Darin McAdams; Matt McCutchen; et al. (Proc. ACM Program. Lang., 2024)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)