Publications By Topic [Show By Year]

Synthesis

Automatic Synthesis of Deterministic Concurrency
Raychev V., Vechev M., Yahav E.
SAS'13: The 20th International Static Analysis Symposium
[pdf] [slides] [TL;DR]
Typestate-Based Semantic Code Search over Partial Programs
Mishne A., Shoham S., Yahav E.
OOPSLA'12:ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages and Applications
[pdf] [slides] [code] [TL;DR]
Dynamic Synthesis for Relaxed Memory Models
Liu F., Nedev N., Prisadnikov N., Vechev M., Yahav E.
PLDI'12:ACM SIGPLAN 2012 Conference on Programming Language Design and Implementation
[pdf] [slides]
Automatic Fine-Grained Locking using Shape Properties
Gueta G., Bronson N., Aiken A., Ramalingam G., Sagiv M., Yahav E.
OOPSLA'11: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
[bib] [abstract] [pdf] [slides]
Partial-Coherence Abstractions for Relaxed Memory Models
Kuperstein M., Vechev M., Yahav E.
PLDI'11:ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation
[bib] [abstract] [pdf] [slides]
Automatic Inference of Memory Fences
Kuperstein M., Vechev M., Yahav E.
SIGACT News: Column 46, Volume 43, Number 2, June 2012
[pdf]
Automatic Inference of Memory Fences
Kuperstein M., Vechev M., Yahav E.
FMCAD '10: Formal Methods in Computer Aided Design
[bib] [abstract] [pdf] [slides]
Verifying Linearizability with Hindsight
O'Hearn P., Rinetzky N., Vechev M., Yahav E., Yorsh G.
PODC '10: Symposium on Principles of Distributed Computing
[bib] [abstract] [pdf] [slides]
Abstraction-Guided Synthesis of Synchronization
Vechev M., Yahav E., Yorsh G.
POPL '10: 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
[bib] [abstract] [pdf] [slides]
Verifying Optimistic Algorithms Should be Easy
Rinetzky N, Vechev M., Yahav E., Yorsh G.
(EC)^2 '09: Exploiting Concurrency Efficiently and Correctly, CAV 2009 Workshop
[pdf]
Experience with Model Checking Linearizability
Vechev M., Yahav E., Yorsh G.
SPIN '09: 16th International SPIN Workshop on Model Checking of Software
[pdf]
Inferring Synchronization Under Limited Observability
Vechev M., Yahav E., Yorsh G.
TACAS '09: 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
[bib] [abstract] [pdf] [slides]
Computer-Assisted Construction of Efficient Concurrent Algorithms
Vechev M., Yahav E., Michael M., Attiya H., Yorsh G.
EC2: Exploiting Concurrency Efficiently and Correctly -- CAV 2008 Workshop
[bib][pdf]
Deriving Linearizable Fine-Grained Concurrent Objects
Vechev M., Yahav E
PLDI '08: ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation.
[bib] [abstract] [pdf] [slides]
CGCExplorer: A Semi-Automated Search Procedure for Provably Correct Concurrent Collectors
Vechev M., Yahav E., Bacon D.F., and Rinetzky N.
PLDI '07: ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation.
[bib] [abstract] [ps] [pdf] [slides]
Correctness-Preserving Derivation of Concurrent Garbage Collection Algorithms
Vechev M., Yahav E., and Bacon D.F.
PLDI '06: ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, June 2006.
[bib][abstract][ps][pdf][slides]

Lightweight Verification

Verifying Determinism of Structured Parallel Programs
Vechev M., Yahav E., Raman R., Sarkar V.
SAS '10: The International Static Analysis Symposium
[bib] [abstract] [pdf] [slides]
Generating Precise and Concise Procedure Summaries
Yorsh G., Yahav E., Chandra S.
POPL'08: ACM Symposium on Principles of Programming Languages
[bib] [abstract] [ps] [pdf] [slides]
Verifying Dereference Safety via Expanding-Scope Analysis
Loginov A., Yahav E., Chandra S., Fink S., Rinetzky N., 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., Yahav E., Chandra S.
ISMM '08: 2008 International Symposium on Memory Management
[bib] [abstract] [pdf] [slides]
The SAFE Experience
Yahav E., Fink S.
In Engineering of Software 2011, Part 1
[pdf]
Static Specification Mining Using Automata-Based Abstractions
Shoham S., Yahav E., Fink S., Pistoia M.
IEEE Transactions on Software Engineering (TSE 2008).
[pdf]
Effective Typestate Verification in the Presence of Aliasing
Fink S.J., Yahav E., Dor N., Ramalingam G., and Geay E.
ACM Transactions on Software Engineering and Methodology 2008 (TOSEM).
[pdf] [code]
Cartesian Partial-Order Reduction
Gueta G., Flanagan C., Yahav E., and Sagiv M.
SPIN '07: 14th Workshop on Model Checking Software
[bib][abstract][pdf]
When Role Models Have Flaws: Static Validation of Enterprise Security Policies
Pistoia M., Fink S.J., Flynn R.J., and Yahav E.
ICSE '07: 29th Int. Conference on Software Engineering.
[bib] [pdf] [slides]
A survey of static analysis methods for identifying security vulnerabilities in software systems
M. Pistoia, S. Chandra, S. J. Fink, and E. Yahav
IBM Systems Journal, volume 46, number 2, Armonk, NY, USA, May 2007
Static Specification Mining Using Automata-Based Abstractions
Shoham S., Yahav E., Fink S., Pistoia M.
ISSTA'07: International Symposium on Software Testing and Analysis 2007
Best paper award
[bib] [abstract] [ps] [pdf] [slides]
Effective Typestate Verification in the Presence of Aliasing
Fink S.J., Yahav E., Dor N., Ramalingam G., and Geay E.
ISSTA '06: International Symposium on Software Testing and Analysis
Best paper award
[bib] [abstract] [ps] [pdf] [slides] [code]
Continuous code-quality assurance with SAFE
Geay E., Yahav E., Fink S.J.
PEPM 2006: ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation
[bib][abstract][pdf]
Establishing Local Temporal Heap Safety Properties with Application to Compile-Time Memory Management
Shaham R., Yahav E., Kolodner E.K., and Sagiv M.,
Science of Computer Programming, Volume 58, Issues 1--2, pages 264-289 , October 2005
Typestate Verification: Abstraction Techniques and Complexity Results
Field J., Goyal D., Ramalingam G., and Yahav E.,
Science of Computer Programming, Volume 58, Issues 1--2, pages 57--82, October 2005
Generating Concrete Counterexamples for Sound Abstract Interpretation,
Erez G., Yahav E., and Sagiv M.
January 2004,[ps][pdf]
Establishing Local Temporal Heap Safety Properties with Application to Compile-Time Memory Management,
Shaham R., Yahav E., Kolodner E.K., and Sagiv M.,
SAS '03 [bib][abstract][ps][pdf][slides]
Typestate Verification: Abstraction Techniques and Complexity Results,
Field J., Goyal D., Ramalingam G., and Yahav E.,
SAS '03  [bib][abstract][ps][pdf][slides]

Quality Aware Runtime

Scalable and Precise Dynamic Datarace Detection for Structured Parallelism
Raman R., Zhao J., Sarkar V., Vechev M., Yahav E.
PLDI'12:ACM SIGPLAN 2012 Conference on Programming Language Design and Implementation
[pdf] [slides]
Testing Atomicity of Composed Concurrent Operations
Shacham O., Bronson N., Aiken A., Sagiv M., Vechev M., Yahav E.
OOPSLA'11: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
[bib] [abstract] [pdf] [slides]
Asynchronous Assertions
Aftandilian E., Guyer S., Vechev M., Yahav E.
OOPSLA'11: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
[bib] [abstract] [pdf] [slides]
Sprint: Speculative Prefetching of Remote Data
Raman A., Yorsh G., Vechev M., Yahav E.
OOPSLA'11: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
to appear
[bib] [abstract] [pdf] [slides]
Efficient Data Race Detection for Async-Finish Parallelism best paper award
Raman R., Zhao J., Sarkar V., Vechev M., Yahav E.
RV '10: International Conference on Runtime Verification
[bib] [abstract] [pdf] [slides]
Parallel Checking of Expressive Heap Assertions
Vechev M., Yahav E., Yorsh G.
ISMM '10: International Symposium on Memory Management
[bib] [abstract] [pdf] [pptx]
Chameleon: Adaptive Selection of Collections
Shacham O., Vechev M., Yahav E.
PLDI '09: ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation.
[bib] [abstract] [pdf] [slides]
to appear
QVM: An Efficient Runtime for Detecting Defects in Deployed Systems
Arnold M., Vechev M., Yahav E.
OOPSLA '08: ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications.
[bib] [abstract] [pdf] [slides] [notes]

Shape Analysis

Verifying Safety Properties of Concurrent Heap-Manipulating Programs
Yahav E. and Sagiv M.
ACM Transactions on Programming Languages and Systems (TOPLAS 2010)
to appear
Modular Verification with Shared Abstractions
Juhasz U., Rinetzky N., Poetzsch-Heffter A., Sagiv M., and Yahav E.
FOOL'09: International Workshop on Foundations of Object-Oriented Languages
[bib][abstract][pdf]
Comparison under Abstraction for Verifying Linearizability
Amit D., Rinetzky N. , Reps T., Sagiv M. and Yahav E.
CAV'07: Computer Aided Verification 2007
[bib][abstract][ps][pdf][slides]
Modular Shape Analysis for Dynamically Encapsulated Programs
Rinetzky N., Poetzsch-Heffter A., Ramalingam G., Sagiv M. , and Yahav E.
ESOP '07: 16th European Symposium on Programming.
[bib][abstract][ps][pdf][slides]
Componentized Heap Abstraction
N. Rinetzky, G. Ramalingam, M. Sagiv, and E. Yahav
TR-164/06, School of Computer Science, Tel Aviv University, December 2006
[pdf]
Verifying Temporal Heap Properties Specified via Evolution Logic
E. Yahav, T. Reps, M. Sagiv, and R. Wilhelm
Logic Journal of IGPL, September 2006
Interprocedural shape analysis for cutpoint-free programs
Rinetzky N., Sagiv M., and Yahav E.
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
Manevich R., Yahav E., Ramalingam G., and Sagiv M.
VMCAI '05: 6th Conference on Verification, Model Checking and Abstract Interpretation, Paris, January 2005
[bib][abstract][ps][pdf][slides]
Property-Guided Verification of Concurrent Heap-Manipulating Programs
Yahav E.
October 2004 [pdf]
Verifying Safety Properties Using Separation and Heterogeneous Abstractions,
Yahav E. and Ramalingam G.
PLDI '04 [bib][abstract][ps][pdf][slides]
Automatically Verifying Concurrent Queue Algorithms,
Yahav E. and Sagiv M.,
SoftMC 2003: Workshop on Software Model Checking
[bib][abstract][ps][pdf][slides]
Verifying Temporal Heap Properties Specified via Evolution Logic
Yahav E., Reps T., Sagiv M., and Wilhelm R.
ESOP '03 [bib][abstract][ps][pdf][supplement][slides]
Verifying Safety Properties of Concurrent Java Programs using 3-Valued Logic
Yahav E.
POPL '01 [bib][abstract][ps][pdf][slides]

Others

High-level Real-time Programming in Java Bacon et.al, ACM EMSOFT 2005
On the Complexity of Partially-Flow-Sensitive Alias Analysis
N. Rinetzky, G. Ramalingam, M. Sagiv, and E. Yahav
ACM Transactions on Programming Languages and Systems (TOPLAS 2008).
[pdf]
Solving The Apprentice Challenge with 3VMC
[bib][abstract][ps][html][pdf] (original challenge by J. Moore)
Compiler Optimization of C++ Virtual Function Calls
Bernstein D. , Fedorov Y., Porat S., Rodrigue J, and Yahav E.
COOTS '96 [bib][abstract][ps][pdf]
(while working as a student employee at IBM Haifa Research Lab).