Travelled to:1 × Canada
1 × China
1 × Croatia
1 × Germany
1 × Ireland
1 × South Korea
1 × Switzerland
1 × United Kingdom
14 × USA
2 × Spain
Collaborated with:W.G.Griswold R.Jhala Z.Tatlock A.Leung R.Tate C.Chambers S.R.Foster M.Shonle M.Stepp S.Kundu J.W.Voung T.D.Millstein R.Gupta R.Chugh M.Das M.Seigle C.Tucker D.Shuffelton J.Sarracino E.R.Scherpelz D.Grove Marc Andrysco J.A.Meister E.Rice A.Sanchez-Stern P.Panchekha D.Ricketts V.Robert D.Jang M.Gupta Y.Agarwal S.Adams T.Ball S.K.Rajamani W.Weimer
Talks about:optim (6) dataflow (4) use (4) synthesi (3) refactor (3) program (3) correct (3) analysi (3) compil (3) proof (3)
Person: Sorin Lerner
DBLP: Lerner:Sorin
Facilitated 1 volumes:
EdContributed to:
2015
20152014
20122012
2011
201120112010
2010200920092008
200820082008
2007200720072005200320022002
2002
2017
201520162018Wrote 30 papers:
- CHI-2015-LernerFG #polymorphism #user interface
- Polymorphic Blocks: Formalism-Inspired UI for Structured Connectors (SL, SRF, WGG), pp. 3063–3072.
- PLDI-2015-LeungSL #interactive #parsing #synthesis
- Interactive parser synthesis by example (AL, JS, SL), pp. 565–574.
- PLDI-2014-RickettsRJTL #automation #proving
- Automating formal proofs for reactive systems (DR, VR, DJ, ZT, SL), p. 47.
- ICSE-2012-FosterGL #ide #named #realtime #refactoring
- WitchDoctor: IDE support for real-time auto-completion of refactorings (SRF, WGG, SL), pp. 222–232.
- PLDI-2012-LeungGAGJL #gpu #kernel #verification
- Verifying GPU kernels by test amplification (AL, MG, YA, RG, RJ, SL), pp. 383–394.
- CAV-2011-SteppTL #validation
- Equality-Based Translation Validator for LLVM (MS, RT, SL), pp. 737–742.
- PLATEAU-2011-ShonleGL #design #using
- Using metaphors from natural discussion to improve the design of arcum (MS, WGG, SL), pp. 39–44.
- PLDI-2011-TateLL #java #type system
- Taming wildcards in Java’s type system (RT, AL, SL), pp. 614–627.
- PLDI-2010-TatlockL #compilation
- Bringing extensibility to verified compilers (ZT, SL), pp. 111–121.
- POPL-2010-TateSL #compilation #generative #optimisation #proving
- Generating compiler optimizations from proofs (RT, MS, SL), pp. 389–402.
- PLDI-2009-ChughMJL #data flow #javascript #staged
- Staged information flow for javascript (RC, JAM, RJ, SL), pp. 50–62.
- PLDI-2009-KunduTL #equivalence #optimisation #proving #using
- Proving optimizations correct using parameterized program equivalence (SK, ZT, SL), pp. 327–337.
- POPL-2009-TateSTL #approach #optimisation #similarity
- Equality saturation: a new approach to optimization (RT, MS, ZT, SL), pp. 264–276.
- CAV-2008-KunduLG #synthesis #validation
- Validating High-Level Synthesis (SK, SL, RG), pp. 459–472.
- OOPSLA-2008-TatlockTSJL #refactoring
- Deep typechecking and refactoring (ZT, CT, DS, RJ, SL), pp. 37–52.
- PASTE-2008-ShonleGL #problem
- Addressing common crosscutting problems with Arcum (MS, WGG, SL), pp. 64–69.
- PLDI-2008-ChughVJL #analysis #concurrent #data flow #detection #source code #using
- Dataflow analysis for concurrent programs using datarace detection (RC, JWV, RJ, SL), pp. 316–326.
- ESEC-FSE-2007-ShonleGL #composition #design #framework #maintenance #refactoring
- Beyond refactoring: a framework for modular maintenance of crosscutting design idioms (MS, WGG, SL), pp. 175–184.
- ESEC-FSE-2007-VoungJL #concurrent #detection #named
- RELAY: static race detection on millions of lines of code (JWV, RJ, SL), pp. 205–214.
- ICSE-2007-TuckerSJL #named
- OPIUM: Optimal Package Install/Uninstall Manager (CT, DS, RJ, SL), pp. 178–188.
- PLDI-2007-ScherpelzLC #automation #semantics
- Automatic inference of optimizer flow functions from semantic meanings (ERS, SL, CC), pp. 135–145.
- POPL-2005-LernerMRC #analysis #automation #data flow #proving
- Automated soundness proofs for dataflow analyses and transformations via local rules (SL, TDM, ER, CC), pp. 364–377.
- PLDI-2003-LernerMC #automation #compilation #correctness #optimisation #proving
- Automatically proving the correctness of compiler optimizations (SL, TDM, CC), pp. 220–231.
- PLDI-2002-DasLS #named #polynomial #verification
- ESP: Path-Sensitive Program Verification in Polynomial Time (MD, SL, MS), pp. 57–68.
- POPL-2002-LernerGC #analysis #data flow
- Composing dataflow analyses and transformations (SL, DG, CC), pp. 270–282.
- SAS-2002-AdamsBDLRSW #analysis #data flow #pointer #using
- Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis (SA, TB, MD, SL, SKR, MS, WW), pp. 230–246.
- ASE-2017-LeungL #ide #named #parsing #synthesis
- Parsimony: an IDE for example-guided synthesis of lexers and parsers (AL, SL), pp. 815–825.
- FDG-2015-FosterLG #integration
- Seamless Integration of Coding and Gameplay: Writing Code Without Knowing it (SRF, SL, WGG).
- POPL-2016-AndryscoJL #float #performance
- Printing floating-point numbers: a faster, always correct method (MA, RJ, SL), pp. 555–567.
- PLDI-2018-Sanchez-SternPL #fault #float
- Finding root causes of floating point error (ASS, PP, SL, ZT), pp. 256–269.