Publications By Year [Show By Topic]

2014

Abstract Semantic Differencing via Speculative Correlation
Nimrod Partush, Eran Yahav
OOPSLA'14: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications
[pdf] [TL;DR]
Tracelet-Based Code Search in Executables
Yaniv David, Eran Yahav
PLDI'14: ACM Conference on Programming Language Design and Implementation
[pdf] [slides] [code] [TL;DR]
Code Completion with Statistical Language Models
Veselin Raychev, Martin Vechev, Eran Yahav
PLDI'14: ACM Conference on Programming Language Design and Implementation
[pdf] [slides] [TL;DR]
Practical concurrent binary search trees via logical ordering
Dana Drachsler, Martin Vechev, Eran Yahav
PPOPP'14: ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming
[pdf] [slides] [code] [TL;DR]
Verifying Atomicity via Data Independence
Ohad Shacham, Eran Yahav, Guy Gueta, Alex Aiken, Nathan Bronson, Mooly Sagiv, Martin Vechev
ISSTA'14: International Symposium on Software Testing and Analysis
[slides]
Synthesis of Memory Fences via Refinement Propagation
Yuri Meshman, Andrei Dan, Martin Vechev, Eran Yahav
SAS'14: The 21th International Static Analysis Symposium
Automatic Semantic Locking (poster)
Guy Gueta, Ramalingam, Mooly Sagiv, Eran Yahav
PPOPP'14: ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming
[pdf] [TL;DR]

2013

Abstract Semantic Differencing for Numerical Programs
Nimrod Partush, Eran Yahav
SAS'13: The 20th International Static Analysis Symposium
[pdf] [slides] [code] [TL;DR]
Predicate Abstraction for Relaxed Memory Models
Andrei Dan, Yuri Meshman, Martin Vechev, Eran Yahav
SAS'13: The 20th International Static Analysis Symposium
[pdf] [slides] [TL;DR]
Symbolic Automata for Specification Mining
Peleg H., Shoham S., Eran Yahav, Yang H.
SAS'13: The 20th International Static Analysis Symposium
[pdf] [slides] [TL;DR]
Automatic Synthesis of Deterministic Concurrency
Veselin Raychev, Martin Vechev, Eran Yahav
SAS'13: The 20th International Static Analysis Symposium
[pdf] [slides] [TL;DR]
Finding Rare Numerical Stability Errors in Concurrent Computations
Hana Chockler, Karine Even, Eran Yahav
ISSTA'13: International Symposium on Software Testing and Analysis
[pdf] [TL;DR]
Concurrent Libraries with Foresight
Guy Gueta, Ramalingam, Mooly Sagiv, Eran Yahav
PLDI'13: ACM Conference on Programming Language Design and Implementation
[pdf] [slides] [TL;DR]

2012

Typestate-Based Semantic Code Search over Partial Programs
Alon Mishne, Sharon Shoham, Eran Yahav
OOPSLA'12:ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications
[pdf] [slides] [code] [codota] [TL;DR]
Dynamic Synthesis for Relaxed Memory Models
Liu F., Nedev N., Prisadnikov N., Martin Vechev, Eran Yahav
PLDI'12:ACM SIGPLAN 2012 Conference on Programming Language Design and Implementation
[pdf] [slides] [TL;DR]
Scalable and Precise Dynamic Datarace Detection for Structured Parallelism
Raghavan Raman, Zhao J., Vivek Sarkar, Martin Vechev, Eran Yahav
PLDI'12:ACM SIGPLAN 2012 Conference on Programming Language Design and Implementation
[pdf] [slides] [TL;DR]
Automatic Inference of Memory Fences
Michael Kuperstein, Martin Vechev, Eran Yahav
SIGACT News: Column 46, Volume 43, Number 2, June 2012
[pdf] [TL;DR]

2011

Automatic Fine-Grained Locking using Shape Properties
Guy Gueta, Nathan Bronson, Alex Aiken, Ramalingam, Mooly Sagiv, Eran Yahav
OOPSLA'11: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
[bib] [abstract] [pdf] [slides] [TL;DR]
Testing Atomicity of Composed Concurrent Operations
Ohad Shacham, Nathan Bronson, Alex Aiken, Mooly Sagiv, Martin Vechev, Eran Yahav
OOPSLA'11: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
[bib] [abstract] [pdf] [slides] [TL;DR]
Asynchronous Assertions
Eddie Aftandilian, Sam Guyer, Martin Vechev, Eran Yahav
OOPSLA'11: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
[bib] [abstract] [pdf] [slides] [TL;DR]
Sprint: Speculative Prefetching of Remote Data
Arun Raman, Greta Yorsh, Martin Vechev, Eran Yahav
OOPSLA'11: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
[bib] [abstract] [pdf] [slides]
Partial-Coherence Abstractions for Relaxed Memory Models
Michael Kuperstein, Martin Vechev, Eran Yahav
PLDI'11:ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation
[bib] [abstract] [pdf] [slides] [TL;DR]
Static Specification Mining using Automata-Based Abstractions
Eran Yahav, Sharon Shoham, Stephen Fink, Marco Pistoia
Book chapter: Mining Software Specifications: Methodologies and Applications
The SAFE Experience
Eran Yahav, Stephen Fink
In Engineering of Software 2011, Part 1
[pdf] [TL;DR]
QVM: An Efficient Runtime for Detecting Defects in Deployed Systems
Matt Arnold, Martin Vechev, Eran Yahav
TOSEM: ACM Transactions on Software Engineering and Methodology, December 2011
[pdf]

2010

Automatic Inference of Memory Fences
Michael Kuperstein, Martin Vechev, Eran Yahav
FMCAD '10: Formal Methods in Computer Aided Design
[bib] [abstract] [pdf] [slides]
Efficient Data Race Detection for Async-Finish Parallelism best paper award
Raman R., Zhao J., Sarkar V., Martin Vechev, Eran Yahav
RV '10: International Conference on Runtime Verification
[bib] [abstract] [pdf] [slides]
Verifying Determinism of Structured Parallel Programs
Martin Vechev, Eran Yahav, Raman R., Sarkar V.
SAS '10: The International Static Analysis Symposium
[bib] [abstract] [pdf] [slides] [TL;DR]
Verifying Linearizability with Hindsight
O'Hearn P., Noam Rinetzky, Martin Vechev, Eran Yahav, Greta Yorsh
PODC '10: Symposium on Principles of Distributed Computing
[bib] [abstract] [pdf] [slides]
Parallel Checking of Expressive Heap Assertions
Martin Vechev, Eran Yahav, Greta Yorsh
ISMM '10: International Symposium on Memory Management
[bib] [abstract] [pdf] [pptx]
Abstraction-Guided Synthesis of Synchronization
Martin Vechev, Eran Yahav, Greta Yorsh
POPL '10: 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
[bib] [abstract] [pdf] [slides] [TL;DR]
Verifying Safety Properties of Concurrent Heap-Manipulating Programs
Eran Yahav and Mooly Sagiv
TOPLAS: ACM Transactions on Programming Languages and Systems (2010)
[pdf]

2009

Chameleon: Adaptive Selection of Collections
Ohad Shacham, Martin Vechev, Eran Yahav
PLDI '09: ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation.
[bib] [abstract] [pdf] [slides]
Inferring Synchronization Under Limited Observability
Martin Vechev, Eran Yahav, Greta Yorsh
TACAS '09: 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
[bib] [abstract] [pdf] [slides]
Experience with Model Checking Linearizability
Martin Vechev, Eran Yahav, Greta Yorsh
SPIN '09: 16th International SPIN Workshop on Model Checking of Software
[pdf]
Modular Verification with Shared Abstractions
Juhasz U., Noam Rinetzky, Poetzsch-Heffter A., Mooly Sagiv, and Eran Yahav
FOOL'09: International Workshop on Foundations of Object-Oriented Languages
[bib][abstract][pdf]
Verifying Optimistic Algorithms Should be Easy
Rinetzky N, Martin Vechev, Eran Yahav, Greta Yorsh
(EC)^2 '09: Exploiting Concurrency Efficiently and Correctly, CAV 2009 Workshop
[pdf]

2008

QVM: An Efficient Runtime for Detecting Defects in Deployed Systems
Arnold M., Martin Vechev, Eran Yahav
OOPSLA '08: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
[bib] [abstract] [pdf] [slides] [notes]
Verifying Dereference Safety via Expanding-Scope Analysis
Loginov A., Eran Yahav, Chandra S., Fink S., Noam Rinetzky, Nanda M. G.
ISSTA '08: International Symposium on Software Testing and Analysis
[bib] [abstract] [pdf] [slides]
The CLOSER: Automating Resource Management in Java
Dillig I., Dillig T., Eran Yahav, Chandra S.
ISMM '08: 2008 International Symposium on Memory Management
[bib] [abstract] [pdf] [slides]
Deriving Linearizable Fine-Grained Concurrent Objects
Martin Vechev, Yahav E
PLDI '08: ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation.
[bib] [abstract] [pdf] [slides]
Generating Precise and Concise Procedure Summaries
Greta Yorsh, Eran Yahav, Chandra S.
POPL'08: ACM Symposium on Principles of Programming Languages
[bib] [abstract] [ps] [pdf] [slides]
Static Specification Mining Using Automata-Based Abstractions
Shoham S., Eran Yahav, Fink S., Pistoia M.
TSE: IEEE Transactions on Software Engineering (2008).
[pdf]
Effective Typestate Verification in the Presence of Aliasing
Fink S.J., Eran Yahav, Dor N., Ramalingam G., and Geay E.
TOSEM: ACM Transactions on Software Engineering and Methodology (2008).
[pdf] [code]
On the Complexity of Partially-Flow-Sensitive Alias Analysis
N. Rinetzky, G. Ramalingam, M. Sagiv, and E. Yahav
TOPLAS: ACM Transactions on Programming Languages and Systems (2008).
[pdf]
Computer-Assisted Construction of Efficient Concurrent Algorithms
Martin Vechev, Eran Yahav, Michael M., Attiya H., Greta Yorsh
(EC)^2: Exploiting Concurrency Efficiently and Correctly -- CAV 2008 Workshop
[bib][pdf]

2007

Static Specification Mining Using Automata-Based Abstractions best paper award Pat Goldberg Best Paper Award
Shoham S., Eran Yahav, Fink S., Pistoia M.
ISSTA'07: International Symposium on Software Testing and Analysis 2007
Best paper award
[bib] [abstract] [ps] [pdf] [slides] [gallery]
Comparison under Abstraction for Verifying Linearizability
Amit D., Noam Rinetzky , Thomas Reps, Mooly Sagiv and Eran Yahav
CAV'07: Computer Aided Verification 2007
[bib] [abstract] [ps] [pdf] [slides]
CGCExplorer: A Semi-Automated Search Procedure for Provably Correct Concurrent Collectors
Martin Vechev, Eran Yahav, David Bacon, and Noam Rinetzky
PLDI '07: ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation.
[bib] [abstract] [ps] [pdf] [slides]
When Role Models Have Flaws: Static Validation of Enterprise Security Policies
Marco Pistoia, Stephen Fink, Robert Flynn, and Eran Yahav
ICSE '07: 29th Int. Conference on Software Engineering.
[bib] [pdf] [slides]
Modular Shape Analysis for Dynamically Encapsulated Programs
Noam Rinetzky, Arnd Poetzsch-Heffter, Ramalingam, Mooly Sagiv , and Eran Yahav
ESOP '07: 16th European Symposium on Programming.
[bib] [abstract] [ps] [pdf] [slides]
A survey of static analysis methods for identifying security vulnerabilities in software systems
Marco Pistoia, Satish Chandra, Stephen Fink, and Eran Yahav
IBM Systems Journal, volume 46, number 2, Armonk, NY, USA, May 2007
Cartesian Partial-Order Reduction
Guy Gueta, Cormac Flanagan, Eran Yahav, and Mooly Sagiv
SPIN '07: 14th Workshop on Model Checking Software
[bib][abstract][pdf]

2006

Effective Typestate Verification in the Presence of Aliasing best paper award
Stephen Fink, Eran Yahav, Nurit Dor, Ramalingam, and Emmanuel Geay
ISSTA '06: International Symposium on Software Testing and Analysis
Best paper award
[bib] [abstract] [ps] [pdf] [slides] [code]
Correctness-Preserving Derivation of Concurrent Garbage Collection Algorithms
Martin Vechev, Eran Yahav, and David Bacon
PLDI '06: ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, June 2006.
[bib] [abstract] [ps] [pdf] [slides]
Verifying Temporal Heap Properties Specified via Evolution Logic
Eran Yahav, Thomas Reps, Mooly Sagiv, and Reinhard Wilhelm
Logic Journal of IGPL, September 2006
Componentized Heap Abstraction
Noam Rinetzky, Ramalingam, Mooly Sagiv, and Eran Yahav
TR-164/06, School of Computer Science, Tel Aviv University, December 2006
[pdf]
Continuous code-quality assurance with SAFE
Emmanuel Geay, Eran Yahav, Stephen Fink
PEPM 2006: ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation
[bib][abstract][pdf]

Earlier...

Interprocedural shape analysis for cutpoint-free programs
Noam Rinetzky, Mooly Sagiv, and Eran Yahav
SAS '05: 12th International Static Analysis Symposium, London, September 7-9, 2005
[bib] [abstract] [ps] [pdf] [slides]
Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists
Roman Manevich, Eran Yahav, Ramalingam, and Mooly Sagiv
VMCAI '05: 6th Conference on Verification, Model Checking and Abstract Interpretation, Paris, January 2005
[bib] [abstract] [ps] [pdf] [slides]
Verifying Safety Properties Using Separation and Heterogeneous Abstractions,
Eran Yahav and Ramalingam
PLDI '04 [bib] [abstract] [ps] [pdf] [slides]
Establishing Local Temporal Heap Safety Properties with Application to Compile-Time Memory Management,
Ran Shaham, Eran Yahav, Kolodner E.K., and Mooly Sagiv,
SAS '03 [bib] [abstract] [ps] [pdf] [slides]
Typestate Verification: Abstraction Techniques and Complexity Results,
John Field, Deepak Goyal, Ramalingam, and Eran Yahav,
SAS '03  [bib] [abstract] [ps] [pdf] [slides]
Verifying Temporal Heap Properties Specified via Evolution Logic
Eran Yahav, Thomas Reps, Mooly Sagiv, and Wilhelm R.
ESOP '03 [bib] [abstract] [ps] [pdf] [supplement] [slides]
Automatically Verifying Concurrent Queue Algorithms,
Eran Yahav and Mooly Sagiv,
SoftMC 2003: Workshop on Software Model Checking
[bib][abstract][ps][pdf][slides]
Verifying Safety Properties of Concurrent Java Programs using 3-Valued Logic
Eran Yahav
POPL '01 [bib] [abstract] [ps] [pdf] [slides]
Compiler Optimization of C++ Virtual Function Calls
Bernstein D. , Fedorov Y., Porat S., Rodrigue J, and Eran Yahav
COOTS '96 [bib][abstract][ps][pdf]
(while working as a student employee at IBM Haifa Research Lab).
Typestate Verification: Abstraction Techniques and Complexity Results
Field J., Goyal D., Ramalingam G., and Eran Yahav,
Science of Computer Programming, Volume 58, Issues 1--2, pages 57--82, October 2005
Establishing Local Temporal Heap Safety Properties with Application to Compile-Time Memory Management
Shaham R., Eran Yahav, Kolodner E.K., and Mooly Sagiv,
Science of Computer Programming, Volume 58, Issues 1--2, pages 264-289 , October 2005

Technical Reports

Symbolic Summarization with Applications to Typestate Verification
Greta Yorsh, Eran Yahav, and Chandra S.
[pdf]
Automatic Verification of Temporal Heap Properties
Eran Yahav, Pnueli A., Thomas Reps, and Mooly Sagiv
January 2004,[ps]
Generating Concrete Counterexamples for Sound Abstract Interpretation,
Erez G., Eran Yahav, and Mooly Sagiv
January 2004,[ps][pdf]
Verifying Safety Properties Using Separation and Heterogeneous Abstractions
Eran Yahav and Ramalingam G.
December 2003[access paper] (revised version appeared in PLDI 2004)
Shallow Finite State Verification,
Field J., Goyal D., Ramalingam G., and Eran Yahav
November 2002 [ps][pdf] (revised version appeared in SAS 2003)
Automatic Verification of Temporal Properties of Concurrent Heap-Manipulating Programs using Evolution Logic
Eran Yahav, Thomas Reps, Mooly Sagiv and Wilhelm R.
TR-338/02, School of Computer Science, Tel Aviv University, July 2002.
[bib][abstract][ps][pdf] (revised version appeared in ESOP 2003)
LTL model checking for systems with unbounded number of dynamically created threads and objects.
Eran Yahav, Thomas Reps, and Mooly Sagiv
TR-1424, Computer Sciences Department, University of Wisconsin, Madison, WI, March 2001.
[bib][abstract][ps][PDF]

Dissertation

Property-Guided Verification of Concurrent Heap-Manipulating Programs
Eran Yahav
October 2004 [pdf]

Misc

High-level Real-time Programming in Java Bacon et.al, ACM EMSOFT 2005
Solving The Apprentice Challenge with 3VMC
[bib][abstract][ps][html][pdf] (original challenge by J. Moore)