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
  • Address: Computer Science Department
    Technion, Haifa 3200003, Israel
  • Office: Taub 734
  • Tel: + 972 4 829 4318

Current Projects

Past Projects


Recent / Selected Publications

Similarity of Binaries through Re-optimization
Synthesis with Abstract Examples
Learning Disjunctions of Predicates
Synthesis of Forgiving Data Extractors
Extracting Code from Programming Tutorial Videos
Leveraging a Corpus of Natural Language Descriptions for Program Similarity
Lossless Separation of Web Pages into Layout Code and Data
Statistical Similarity of Binaries
Cross-Supervised Synthesis of Web-Crawlers
D3 : Data-Driven Disjunctive Abstraction
Estimating Types in Binaries using Predictive Modeling
Code Similarity via Natural Language Descriptions [slides] [talk]
Exploiting Social Navigation (BlackHat Asia)
Automatic Scalable Atomicity via Semantic Locking
Effective Abstractions for Verification under Relaxed Memory Models
Abstract Semantic Differencing via Speculative Correlation [code]
Tracelet-Based Code Search in Executables [code]
Code Completion with Statistical Language Models
Practical concurrent binary search trees via logical ordering [code]
Automatic semantic locking
Synthesis of Memory Fences via Refinement Propagation
Automatic Synthesis of Deterministic Concurrency
Predicate Abstraction for Relaxed Memory Models
Abstract Semantic Differencing for Numerical Programs [code]
Symbolic Automata for Specification Mining
Concurrent Libraries with Foresight
Typestate-Based Semantic Code Search over Partial Programs [code]
Dynamic Synthesis for Relaxed Memory Models
Scalable and Precise Dynamic Datarace Detection for Structured Parallelism
Testing Atomicity of Composed Concurrent Operations
Automatic Fine-Grained Locking using Shape Properties
Asynchronous Assertions
Partial-Coherence Abstractions for Relaxed Memory Models
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 techniques for programming with millions of examples by learning from available public code. PRIME combines static analysis and machine learning techniques to effectively answer semantic code-search queries, code prediction, code completion, and similarity queries. (OOPSLA'12) (SAS'13) (PLDI'14a) (PLDI'14b) (OOPSLA'14) (POPL'16) (PLDI'16) (ICSE'16) (ONWARD'16a)(ONWARD'16b) (PLDI'17) (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


Go Top


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


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


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