Travelled to:1 × Canada
1 × Finland
1 × Portugal
1 × Slovenia
1 × South Africa
1 × United Kingdom
5 × USA
Collaborated with:R.Bodík J.Bornholt D.Jackson S.Chandra M.D.Ernst J.Dolby ∅ P.Panchekha S.Pernsteiner C.Loncaric S.Barman M.Vaziri F.S.Chang J.Edwards J.Toman E.Butler Z.Popovic A.Krishnamurthy S.Chang Alex Knauth Z.Tatlock X.W.0005 D.Grossman L.Ceze M.Schäfer M.Sridharan F.Tip A.Bhattacharya D.Culler K.Weitz D.Woos A.Kaufmann J.Li J.Jacky P.M.Phothilimthana Archibald Samuel Elliott An Wang 0003 Abhinav Jangda Bastian Hagedorn Henrik Barthels Samuel J. Kaufman V.Grover
Talks about:model (7) synthesi (4) symbol (4) solver (4) synthes (3) system (3) scalabl (2) languag (2) specif (2) memori (2)
Person: Emina Torlak
DBLP: Torlak:Emina
Facilitated 1 volumes:
EdContributed to:
2015
20142013
2012
2012
2011
201020102010
2008
20072004
20152016
2017
201620182016
201620172018
20162019Wrote 24 papers:
- Onward-2015-BarmanBCTBC #interactive #synthesis #tool support #towards
- Toward tool support for interactive synthesis (SB, RB, SC, ET, AB, DC), pp. 121–136.
- PLDI-2014-TorlakB #lightweight #virtual machine
- A lightweight symbolic virtual machine for solver-aided host languages (ET, RB), p. 54.
- Onward-2013-TorlakB
- Growing solver-aided languages with rosette (ET, RB), pp. 135–152.
- CAV-2012-BodikT #constraints #source code #theorem proving
- Synthesizing Programs with Constraint Solvers (RB, ET), p. 3.
- FSE-2012-Torlak #generative #modelling #multi #scalability #testing
- Scalable test data generation from multidimensional models (ET), p. 36.
- ICSE-2011-ChandraTBB #debugging
- Angelic debugging (SC, ET, SB, RB), pp. 121–130.
- ECOOP-2010-SchaferDSTT #concurrent #java #refactoring
- Correct Refactoring of Concurrent Java Code (MS, JD, MS, ET, FT), pp. 225–249.
- ICSE-2010-TorlakC #detection #effectiveness #interprocedural
- Effective interprocedural resource leak detection (ET, SC), pp. 535–544.
- PLDI-2010-TorlakVD #axiom #memory management #modelling #named #specification
- MemSAT: checking axiomatic specifications of memory models (ET, MV, JD), pp. 341–350.
- FM-2008-TorlakCJ #declarative #satisfiability #specification
- Finding Minimal Unsatisfiable Cores of Declarative Specifications (ET, FSHC, DJ), pp. 326–341.
- TACAS-2007-TorlakJ #named #relational
- Kodkod: A Relational Model Finder (ET, DJ), pp. 632–647.
- FSE-2004-EdwardsJT #modelling #type system
- A type system for object models (JE, DJ, ET), pp. 189–199.
- ASE-2015-TomanPT #bound #named #rust #verification
- Crust: A Bounded Verifier for Rust (N) (JT, SP, ET), pp. 75–80.
- CAV-2016-PernsteinerLTTW #modelling #safety #using
- Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers (SP, CL, ET, ZT, XW0, MDE, JJ), pp. 23–41.
- FDG-2017-ButlerTP #game studies
- Synthesizing interpretable strategies for solving puzzle games (EB, ET, ZP), p. 10.
- OOPSLA-2016-PanchekhaT #automation #layout #reasoning #web
- Automated reasoning for web page layout (PP, ET), pp. 181–194.
- OOPSLA-2016-WeitzWTEKT #protocol #scalability #smt #verification
- Scalable verification of border gateway protocol configurations with an SMT solver (KW, DW, ET, MDE, AK, ZT), pp. 765–780.
- OOPSLA-2018-BornholtT #evaluation #symbolic computation
- Finding code that explodes under symbolic evaluation (JB, ET), p. 26.
- PLDI-2016-LoncaricTE #performance #synthesis
- Fast synthesis of fast collections (CL, ET, MDE), pp. 355–368.
- POPL-2016-BornholtTGC #optimisation #sketching #synthesis
- Optimizing synthesis with metasketches (JB, ET, DG, LC), pp. 775–788.
- PLDI-2017-BornholtT #framework #memory management #modelling #sketching #testing
- Synthesizing memory models from framework sketches and Litmus tests (JB, ET), pp. 467–481.
- POPL-2018-ChangKT #execution #symbolic computation
- Symbolic types for lenient symbolic execution (SC, AK, ET), p. 29.
- ASPLOS-2016-BornholtKLKTW #file system #modelling #specification
- Specifying and Checking File System Crash-Consistency Models (JB, AK, JL, AK, ET, XW0), pp. 83–98.
- ASPLOS-2019-PhothilimthanaE #data flow #gpu #kernel #synthesis
- Swizzle Inventor: Data Movement Synthesis for GPU Kernels (PMP, ASE, AW0, AJ, BH, HB, SJK, VG, ET, RB), pp. 65–78.