Travelled to:
1 × China
1 × India
1 × Ireland
1 × Italy
1 × Poland
1 × Portugal
1 × Spain
1 × Switzerland
2 × Canada
2 × France
2 × Germany
20 × USA
5 × United Kingdom
Collaborated with:
M.T.Vechev N.Partush M.Sagiv G.Ramalingam G.Yorsh ∅ Y.David N.Rinetzky S.Shoham G.Golan-Gueta Meital Zilberstein S.J.Fink A.M.Dan Y.Meshman S.Chandra S.Sagiv V.Raychev Omer Katz O.Shacham D.F.Bacon E.Geay M.Pistoia Shir Yadid Uri Alon 0002 Omer Levy A.Aiken N.G.Bronson R.Raman V.Sarkar T.W.Reps G.Ramalingam S.Fink D.Drachsler H.Chockler K.Even A.Mishne M.Kuperstein M.Arnold D.Drachsler-Cohen R.El-Yaniv H.Peleg H.Yang E.Aftandilian S.Z.Guyer A.Raman I.Dillig T.Dillig R.J.Flynn R.Manevich R.Wilhelm J.Field D.Goyal R.Shaham E.K.Kolodner F.Liu N.Nedev N.Prisadnikov J.Zhao D.Amit A.Poetzsch-Heffter N.Dor A.Loginov M.G.Nanda
Talks about:
abstract (14) program (10) concurr (9) model (8) code (7) synthesi (6) properti (6) verifi (6) memori (6) automat (5)
Person: Eran Yahav
DBLP: Yahav:Eran
Facilitated 1 volumes:
Contributed to:
Wrote 60 papers:
- PPoPP-2015-Golan-GuetaRSY #automation #scalability #semantics
- Automatic scalable atomicity via semantic locking (GGG, GR, MS, EY), pp. 31–41.
- VMCAI-2015-DanMVY #abstraction #effectiveness #memory management #modelling #verification
- Effective Abstractions for Verification under Relaxed Memory Models (AMD, YM, MTV, EY), pp. 449–466.
- ISSTA-2014-ShachamYGABSV #independence #verification
- Verifying atomicity via data independence (OS, EY, GGG, AA, NGB, MS, MTV), pp. 26–36.
- OOPSLA-2014-PartushY #correlation #difference #semantics
- Abstract semantic differencing via speculative correlation (NP, EY), pp. 811–828.
- PLDI-2014-DavidY #bytecode #code search
- Tracelet-based code search in executables (YD, EY), p. 37.
- PLDI-2014-RaychevVY #code completion #modelling #statistics
- Code completion with statistical language models (VR, MTV, EY), p. 44.
- PPoPP-2014-DrachslerVY #concurrent #logic
- Practical concurrent binary search trees via logical ordering (DD, MTV, EY), pp. 343–356.
- PPoPP-2014-Golan-GuetaRSY #automation #semantics
- Automatic semantic locking (GGG, GR, MS, EY), pp. 385–386.
- SAS-2014-MeshmanDVY #memory management #refinement #synthesis
- Synthesis of Memory Fences via Refinement Propagation (YM, AMD, MTV, EY), pp. 237–252.
- ISSTA-2013-ChocklerEY #concurrent #fault
- Finding rare numerical stability errors in concurrent computations (HC, KE, EY), pp. 12–22.
- PLDI-2013-Golan-GuetaRSY #concurrent #library
- Concurrent libraries with foresight (GGG, GR, MS, EY), pp. 263–274.
- SAS-2013-DanMVY #abstraction #memory management #modelling
- Predicate Abstraction for Relaxed Memory Models (AMD, YM, MTV, EY), pp. 84–104.
- SAS-2013-PartushY #difference #semantics #source code
- Abstract Semantic Differencing for Numerical Programs (NP, EY), pp. 238–258.
- SAS-2013-PelegSYY #automaton #mining #specification
- Symbolic Automata for Static Specification Mining (HP, SS, EY, HY), pp. 63–83.
- SAS-2013-RaychevVY #automation #concurrent #synthesis
- Automatic Synthesis of Deterministic Concurrency (VR, MTV, EY), pp. 283–303.
- VMCAI-2013-Yahav #synthesis
- Abstraction-Guided Synthesis (EY), p. 27.
- OOPSLA-2012-MishneSY #code search #semantics #source code
- Typestate-based semantic code search over partial programs (AM, SS, EY), pp. 997–1016.
- PLDI-2012-LiuNPVY #memory management #modelling #synthesis
- Dynamic synthesis for relaxed memory models (FL, NN, NP, MTV, EY), pp. 429–440.
- PLDI-2012-RamanZSVY #concurrent #detection #parallel #precise #scalability
- Scalable and precise dynamic datarace detection for structured parallelism (RR, JZ, VS, MTV, EY), pp. 531–542.
- OOPSLA-2011-AftandilianGVY
- Asynchronous assertions (EA, SZG, MTV, EY), pp. 275–288.
- OOPSLA-2011-Golan-GuetaBARSY #automation #using
- Automatic fine-grain locking using shape properties (GGG, NGB, AA, GR, MS, EY), pp. 225–242.
- OOPSLA-2011-RamanYVY #named
- Sprint: speculative prefetching of remote data (AR, GY, MTV, EY), pp. 259–274.
- OOPSLA-2011-ShachamBASVY #concurrent #testing
- Testing atomicity of composed concurrent operations (OS, NGB, AA, MS, MTV, EY), pp. 51–64.
- PLDI-2011-KupersteinVY #abstraction #memory management #modelling
- Partial-coherence abstractions for relaxed memory models (MK, MTV, EY), pp. 187–198.
- ISMM-2010-VechevYY #named #parallel
- PHALANX: parallel checking of expressive heap assertions (MTV, EY, GY), pp. 41–50.
- POPL-2010-VechevYY #synthesis
- Abstraction-guided synthesis of synchronization (MTV, EY, GY), pp. 327–338.
- SAS-2010-VechevYRS #automation #parallel #source code #verification
- Automatic Verification of Determinism for Structured Parallel Programs (MTV, EY, RR, VS), pp. 455–471.
- PLDI-2009-ShachamVY #adaptation #named
- Chameleon: adaptive selection of collections (OS, MTV, EY), pp. 408–418.
- TACAS-2009-VechevYY
- Inferring Synchronization under Limited Observability (MTV, EY, GY), pp. 139–154.
- ISMM-2008-DilligDYC #automation #java #resource management
- The CLOSER: automating resource management in java (ID, TD, EY, SC), pp. 1–10.
- ISSTA-2008-LoginovYCFRN #analysis #safety #verification
- Verifying dereference safety via expanding-scope analysis (AL, EY, SC, SF, NR, MGN), pp. 213–224.
- OOPSLA-2008-ArnoldVY #detection #fault #named #performance #runtime
- QVM: an efficient runtime for detecting defects in deployed systems (MA, MTV, EY), pp. 143–162.
- PLDI-2008-VechevY #concurrent #fine-grained
- Deriving linearizable fine-grained concurrent objects (MTV, EY), pp. 125–135.
- POPL-2008-YorshYC #generative #precise #summary
- Generating precise and concise procedure summaries (GY, EY, SC), pp. 221–234.
- CAV-2007-AmitRRSY #abstraction #comparison #verification
- Comparison Under Abstraction for Verifying Linearizability (DA, NR, TWR, MS, EY), pp. 477–490.
- ESOP-2007-RinetzkyPRSY #analysis #composition #encapsulation #source code
- Modular Shape Analysis for Dynamically Encapsulated Programs (NR, APH, GR, MS, EY), pp. 220–236.
- ICSE-2007-PistoiaFFY #enterprise #modelling #policy #security #validation
- When Role Models Have Flaws: Static Validation of Enterprise Security Policies (MP, SJF, RJF, EY), pp. 478–488.
- ISSTA-2007-ShohamYFP #abstraction #mining #specification #using
- Static specification mining using automata-based abstractions (SS, EY, SF, MP), pp. 174–184.
- PLDI-2007-VechevYBR #automation #concurrent #named
- CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors (MTV, EY, DFB, NR), pp. 456–467.
- ISSTA-2006-FinkYDRG #alias #effectiveness #type system #verification
- Effective typestate verification in the presence of aliasing (SJF, EY, ND, GR, EG), pp. 133–144.
- PEPM-2006-GeayYF #assurance #quality
- Continuous code-quality assurance with SAFE (EG, EY, SJF), pp. 145–149.
- PLDI-2006-VechevYB #algorithm #concurrent #garbage collection
- Correctness-preserving derivation of concurrent garbage collection algorithms (MTV, EY, DFB), pp. 341–353.
- SAS-2005-RinetzkySY #analysis #interprocedural #source code
- Interprocedural Shape Analysis for Cutpoint-Free Programs (NR, MS, EY), pp. 284–302.
- VMCAI-2005-ManevichYRS #abstraction #canonical
- Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists (RM, EY, GR, SS), pp. 181–198.
- PLDI-2004-YahavR #abstraction #safety #using #verification
- Verifying safety properties using separation and heterogeneous abstractions (EY, GR), pp. 25–34.
- ESOP-2003-YahavRSW #evolution #logic #verification
- Verifying Temporal Heap Properties Specified via Evolution Logic (EY, TWR, SS, RW), pp. 204–222.
- SAS-2003-FieldGRY #abstraction #complexity #type system #verification
- Typestate Verification: Abstraction Techniques and Complexity Results (JF, DG, GR, EY), pp. 439–462.
- SAS-2003-ShahamYKS #memory management #safety
- Establishing Local Temporal Heap Safety Properties with Applications to Compile-Time Memory Management (RS, EY, EKK, SS), pp. 483–503.
- POPL-2001-Yahav #concurrent #java #logic #safety #source code #using #verification
- Verifying safety properties of concurrent Java programs using 3-valued logic (EY), pp. 27–40.
- CAV-2017-Drachsler-Cohen #synthesis
- Synthesis with Abstract Examples (DDC, SS, EY), pp. 254–278.
- CAV-2018-Yahav #modelling #source code
- From Programs to Interpretable Deep Models and Back (EY), pp. 27–37.
- Onward-2016-YadidY #programming #tutorial
- Extracting code from programming tutorial videos (SY, EY), pp. 98–111.
- Onward-2016-ZilbersteinY #corpus #natural language #similarity
- Leveraging a corpus of natural language descriptions for program similarity (MZ, EY), pp. 197–211.
- PLDI-2016-DavidPY #similarity #statistics
- Statistical similarity of binaries (YD, NP, EY), pp. 266–280.
- POPL-2016-KatzEY #modelling #predict #using
- Estimating types in binaries using predictive modeling (OK, REY, EY), pp. 313–326.
- PLDI-2017-DavidPY #similarity
- Similarity of binaries through re-optimization (YD, NP, EY), pp. 79–94.
- PLDI-2018-0002ZLY #predict #representation
- A general path-based representation for predicting program properties (UA0, MZ, OL, EY), pp. 404–419.
- POPL-2019-AlonZLY #distributed #learning #named
- code2vec: learning distributed representations of code (UA0, MZ, OL, EY), p. 29.
- ASPLOS-2018-DavidPY #detection #named #precise #static analysis
- FirmUp: Precise Static Detection of Common Vulnerabilities in Firmware (YD, NP, EY), pp. 392–404.
- ASPLOS-2018-KatzRY #re-engineering #statistics
- Statistical Reconstruction of Class Hierarchies in Binaries (OK, NR, EY), pp. 363–376.