Eran Yahav

Faculty member at the Computer Science Department, Technion, Israel.

Research Interests

  • Program synthesis, machine learning and information-retrieval techniques for PL
  • Program analysis, abstract interpretation, verification
  • Programming Languages, software engineering

Contact Information

  • Eran Yahav E-mail yahave@cs.technion.ac.il
  • Address: Computer Science Department
    Technion, Haifa 3200003, Israel
  • Office: Taub 734
  • Tel: + 972 4 829 4318

Current Projects

Past Projects

Software

Recent / Selected Publications

ONWARD'16
Extracting Code from Programming Tutorial Videos
ONWARD'16
Leveraging a Corpus of Natural Language Descriptions for Program Similarity
KDD'16
Lossless Separation of Web Pages into Layout Code and Data
PLDI'16
Statistical Similarity of Binaries
ICSE'16
Cross-Supervised Synthesis of Web-Crawlers
VMCAI'16
D3 : Data-Driven Disjunctive Abstraction
POPL'16
Estimating Types in Binaries using Predictive Modeling
OBT'15
Code Similarity via Natural Language Descriptions [slides] [talk]
BlackHat'15
Exploiting Social Navigation (BlackHat Asia)
PPOPP'15
Automatic Scalable Atomicity via Semantic Locking
VMCAI'15
Effective Abstractions for Verification under Relaxed Memory Models
OOPSLA14
Abstract Semantic Differencing via Speculative Correlation [code]
PLDI14
Tracelet-Based Code Search in Executables [code]
PLDI14
Code Completion with Statistical Language Models
PPOPP14
Practical concurrent binary search trees via logical ordering [code]
PPOPP14
Automatic semantic locking
SAS14
Synthesis of Memory Fences via Refinement Propagation
SAS13
Automatic Synthesis of Deterministic Concurrency
SAS13
Predicate Abstraction for Relaxed Memory Models
SAS13
Abstract Semantic Differencing for Numerical Programs [code]
SAS13
Symbolic Automata for Specification Mining
PLDI13
Concurrent Libraries with Foresight
OOPSLA12
Typestate-Based Semantic Code Search over Partial Programs [code]
PLDI12
Dynamic Synthesis for Relaxed Memory Models
PLDI12
Scalable and Precise Dynamic Datarace Detection for Structured Parallelism
OOPSLA11
Testing Atomicity of Composed Concurrent Operations
OOPSLA11
Automatic Fine-Grained Locking using Shape Properties
OOPSLA11
Asynchronous Assertions
PLDI11
Partial-Coherence Abstractions for Relaxed Memory Models
POPL10
Abstraction-Guided Synthesis of Synchronization
Go Top

Research: Current Projects

PRIME: Programming with Millions of Examples

Programmers make extensive use of frameworks and libraries. To perform standard tasks, such as parsing an XML file or communicating with a database, programmers use standard frameworks rather than writing code from scratch. Unfortunately, a typical framework API can involve hundreds of classes with dozens of methods each, and often requires specific sequences of operations that have to be invoked on specific objects in order to perform a single task. Even experienced programmers might spend hours trying to understand how to use a seemingly simple API. The goal of PRIME is to develop a semantic search-engine that can answer semantic code-search queries, dealing with how an API is used, in a way that consolidates, distills, and ranks matching code snippets. PRIME combines static analysis and machine learning techniques to effectively answer semantic code-search queries. (OOPSLA'12) (SAS'13) (PLDI'14a) (PLDI'14b) (OOPSLA'14) (POPL'16) (PLDI'16) (ICSE'16) (ONWARD'16a)(ONWARD'16b) (talk video) (PRIME code) (TRACY code) (codota)

Research: Past Projects

Fender: Preserving Correctness under Weak Memory Models

Modern architectures implement relaxed memory models in which memory operations may be reordered and executed nonatomically. Special instructions called memory fences are provided to the programmer, allowing control of this behavior. To ensure correctness of many algorithms, in particular of non-blocking ones, a programmer is often required to explicitly insert memory fences into her program. However, she must use as few fences as possible, or the benefits of running on a relaxed architecture will be lost. Placing memory fences is challenging and extremely error prone, as it requires subtle reasoning about the underlying memory model. The goal of this project is to automatically infer memory fences in concurrent programs, assisting the programmer with this complex task.
(FMCAD'10) (PLDI'11) (PLDI'12) (SA-News'12) (SAS'13) (SAS'14) (DFence Code)

Saint: Synthesis using Abstract Interpretation

Can we generate synchronization code for a program based on a high-level specification of its desired behavior? In this project, we turn the one dimensional problem of verification under abstraction, in which only the abstraction can be modified (typically via abstraction refinement), into a two-dimensional problem, in which both the program and the abstraction can be modified until the abstraction is precise enough to verify the program. We are interested in modifications of a concurrent program that restrict its possible interleavings.
(TACAS'09) (EC2 '09) (SPIN '09) (POPL'10)

Dojo: Ensuring Determinism of Concurrent Systems

One of the main difficulties in parallel programming is the need to reason about possible interleavings of operations in a program. The vast number of interleavings makes this task difficult even for small programs, and impossible for any sizeable software. To simplify reasoning about parallel programs, it is desirable to reduce the number of interleavings that a programmer has to consider. One way to achieve that is to require parallel programs to be deterministic. The goal of this project is to investigate static and dynamic program analysis techniques for checking and enforcing determinism in concurrent systems.
(SAS'10) (RV'10 best paper award) (PLDI'12)

QVM: The Quality Virtual Machine

The Quality Virtual Machine (QVM) is a system that uses the technology and infrastructure available in a virtual machine to improve software quality. QVM provides a framework for easily building dynamic analyses into the VM, continuing the general trend of using additional hardware resources at runtime to help find and/or eliminate bugs.
(OOPSLA'08) (PLDI'09) (ISMM'10) (OOPSLA'11)

Paraglide: Search-Based Synthesis of Concurrent Programs

Current practices for developing concurrent systems are rather limited. Manual constructions using low-level concurrency constructs (e.g. CAS) is the realm of experts, is extremely error-prone and leads to significant non-repeatable effort in both the construction and the verification process. Generic higher-level constructs (e.g., transactional memory) are also limited, and are not clearly easier to use. Analytic techniques (e.g., race detection) only address a fraction of the problems, and can only be applied after the code is written at which point it may be broken beyond repair. The Paraglide project provides construction mechanisms and practical tools that assist the designer in building correct and efficient concurrent systems.
(PLDI'06) (PLDI'07) (PLDI'08) (EC2 '08)

SAFE: Scalable Verification for Heap-Manipulating Programs

The goal of SAFE is to provide a scalable and flexible error-detection tool, based on typestate checking with varying degrees of cost and precision, mostly depending on the way in which aliasing is handled. SAFE can be used for detecting violations of simple correctness properties, and for checking more sophisticated performance properties such as inefficient use of resources.
(ISSTA'06 best paper award) (ISSTA'07 best paper award Pat Goldberg Best Paper Award) (POPL'08) (ISMM'08) (ISSTA'08) (TSE'08) (TOSEM'08) (Mining'11) (Exp'11)

3VMC/TVLA: Shape Analysis for Concurrent Programs

3VMC is a tool for analysis and verification of concurrent systems. 3VMC is geared towards verification of concurrent software, it supports dynamic allocation of objects and threads and does not put an a priori bound on the number of allocated objects and threads.
(POPL'01) (SOFTMC'03) (ESOP'03) (PLDI'04) (IGPL'08) (TOPLAS'10)

Go Top

Publications

Go Top

Students

Current Students

Past Students

Undergraduate Students

Summer Interns

  • Nayden Nedev, Sofia University, Bulgaria (2010) - with Martin Vechev
    Dynamic Synthesis of Memory Fences (PLDI'12)

  • Nedyalko Prisadnikov, Sofia University, Bulgaria (2010) - with Martin Vechev
    Dynamic Synthesis of Memory Fences (PLDI'12)

  • Raghavan Raman, Rice University (2009) - with Martin Vechev
    Checking and Verifying Determinism (SAS'10, RV'10 best paper)

  • Ohad Shacham, Tel Aviv University, Israel (2008) - with Martin Vechev
    Chameleon: Adaptive Selection of Collections (PLDI'09) , also won 2nd place in PLDI'09 SRC.

  • Isil Dillig, Stanford (2007) - with Satish Chandra
    The CLOSER: Automating Resource Management in Java (ISMM'08)

  • Thomas Dillig, Stanford (2007) - with Satish Chandra
    The CLOSER: Automating Resource Management in Java (ISMM'08)

  • Greta Yorsh, Tel Aviv University, Israel (2006)
    Modular Analysis
    Generating Precise and Concise Procedure Summaries (POPL'08)

  • Sharon Shoham, Technion - Israel Institute of Technology (2006, visit 2007)
    Mining Temporal Specification
    (ISSTA'07 best paper)

  • Martin Vechev, Cambridge University (2005, 2006)
    Synthesis of Concurrent Garbage Collectors (PLDI'06) (PLDI'07)

  • Noam Rinetzky, Tel Aviv Univeristy, Israel (2005)
    Misc. Shape Analysis Problems (TOPLAS'07)

Go Top

Courses

Winter 2016-2017

  • Advanced Course in Program Analysis and Synthesis (236347)
  • Software Project - Android Applications (236504)

Spring 2016

Winter 2015-2016

  • Advanced Course in Program Analysis and Synthesis (236347)
  • Software Project - Android Applications (236504)

Spring 2015

Winter 2014-2015

  • Advanced Course in Program Analysis and Synthesis (236347)
  • Software Project - Android Applications (236504)

Spring 2014

Winter 2013-2014

Spring 2013

Winter 2012-2013

Spring 2012

Winter 2011

Spring 2011

Spring 2010

Go Top

Activities

Professional Activities

Current/Recent: Others: VSSE'13 (Talk) Marktoberdorf International Summer School 2013 ESOP'13 (PC) APLAS'12 (PC) SYNTH'12 (PC) WoDet'12 (PC) ISMM'12 (XRC) Dagstuhl Seminar on Software Synthesis (Co-organizer) LFX 2010: Learning From eXperience (co-organizer) TAPAS 2010: Tools for Automatic Program AnalysiS, ICSE NIER 2010, VEE 2010, ISSTA 2009 (PC), HVC 2009, DEFECTS 2009, CSR 2009, ISMM 2009 RC, BYTECODE 2009, HAV 2008, SPIN 2008, SPACE 2008, HAV 2007, PASSWORD 2006

Selected Talks

Other Activities

Go Top
Go Top