Publications By Year [Show By Topic]
2013
| Abstract Semantic Differencing for Numerical Programs Partush N., Yahav E. SAS'13: The 20th International Static Analysis Symposium [pdf] [slides] [TL;DR] |
| Predicate Abstraction for Relaxed Memory Models Dan A., Meshman Y., Vechev M., Yahav E. SAS'13: The 20th International Static Analysis Symposium [pdf] [slides] [TL;DR] |
| Symbolic Automata for Specification Mining Peleg H., Shoham S., Yahav E., Yang H. SAS'13: The 20th International Static Analysis Symposium [pdf] [slides] [TL;DR] |
| Automatic Synthesis of Deterministic Concurrency Raychev V., Vechev M., Yahav E. SAS'13: The 20th International Static Analysis Symposium [pdf] [slides] [TL;DR] |
| Concurrent Libraries with Foresight Gueta G., Ramalingam, Sagiv M., Yahav E. PLDI'13: ACM Conference on Programming Language Design and Implementation [pdf] [slides] [TL;DR] |
2012
| 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] [TL;DR] |
| 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] [TL;DR] |
| Automatic Inference of Memory Fences Kuperstein M., Vechev M., Yahav E. SIGACT News: Column 46, Volume 43, Number 2, June 2012 [pdf] [TL;DR] |
2011
| 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] [TL;DR] |
| 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] [TL;DR] |
| 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] [TL;DR] |
| 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. [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] [TL;DR] |
| Static Specification Mining using Automata-Based Abstractions Yahav E., Shoham S., Fink S., Pistoia M. Book chapter: Mining Software Specifications: Methodologies and Applications |
| The SAFE Experience Yahav E., Fink S. In Engineering of Software 2011, Part 1 [pdf] [TL;DR] |
| QVM: An Efficient Runtime for Detecting Defects in Deployed Systems Arnold M., Vechev M., Yahav E. TOSEM: ACM Transactions on Software Engineering and Methodology, December 2011 [pdf] |
2010
| Automatic Inference of Memory Fences Kuperstein M., Vechev M., Yahav E. FMCAD '10: Formal Methods in Computer Aided Design [bib] [abstract] [pdf] [slides] |
Efficient Data Race Detection for Async-Finish Parallelism
 Raman R., Zhao J., Sarkar V., Vechev M., Yahav E. RV '10: International Conference on Runtime Verification [bib] [abstract] [pdf] [slides] |
| 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] [TL;DR] |
| 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] |
| Parallel Checking of Expressive Heap Assertions Vechev M., Yahav E., Yorsh G. ISMM '10: International Symposium on Memory Management [bib] [abstract] [pdf] [pptx] |
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] [TL;DR] |
| Verifying Safety Properties of Concurrent Heap-Manipulating Programs
Yahav E. and Sagiv M. TOPLAS: ACM Transactions on Programming Languages and Systems (2010) [pdf] |
2009
| 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] |
| 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] |
| Experience with Model Checking Linearizability Vechev M., Yahav E., Yorsh G. SPIN '09: 16th International SPIN Workshop on Model Checking of Software [pdf] |
| 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] |
| 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] |
2008
| 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] |
|
| 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] |
|
| 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] |
|
| 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] |
|
| Static Specification Mining Using Automata-Based Abstractions Shoham S., Yahav E., Fink S., Pistoia M. TSE: IEEE Transactions on Software Engineering (2008). [pdf] |
|
| Effective Typestate Verification in the Presence of Aliasing Fink S.J., Yahav E., 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 Vechev M., Yahav E., Michael M., Attiya H., Yorsh G. (EC)^2: Exploiting Concurrency Efficiently and Correctly -- CAV 2008 Workshop [bib][pdf] |
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] [gallery] |
|
| 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] |
|
| 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] |
|
| 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] |
|
| 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] |
|
| 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 | |
| Cartesian Partial-Order Reduction Gueta G., Flanagan C., Yahav E., and Sagiv M. SPIN '07: 14th Workshop on Model Checking Software [bib][abstract][pdf] |
2006
| 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] |
| 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] |
| Verifying Temporal Heap Properties Specified via Evolution Logic
E. Yahav, T. Reps, M. Sagiv, and R. Wilhelm Logic Journal of IGPL, September 2006 |
| 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] |
| 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] |
Earlier...
| 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] |
| Verifying Safety Properties Using Separation and Heterogeneous
Abstractions, Yahav E. and Ramalingam G. PLDI '04 [bib] [abstract] [ps] [pdf] [slides] |
| 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] |
| 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] |
| Automatically Verifying Concurrent Queue Algorithms,
Yahav E. and Sagiv M., SoftMC 2003: Workshop on Software Model Checking [bib][abstract][ps][pdf][slides] |
| Verifying Safety Properties of Concurrent Java Programs using 3-Valued Logic
Yahav E. POPL '01 [bib] [abstract] [ps] [pdf] [slides] |
| 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). |
| 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 |
| 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 |
Technical Reports
| Symbolic Summarization with Applications to Typestate Verification Yorsh G., Yahav E., and Chandra S. [pdf] |
| Automatic Verification of Temporal Heap Properties Yahav E., Pnueli A., Reps T., and Sagiv M. January 2004,[ps] |
| Generating Concrete Counterexamples for Sound Abstract
Interpretation, Erez G., Yahav E., and Sagiv M. January 2004,[ps][pdf] |
| Verifying Safety Properties Using Separation and Heterogeneous
Abstractions Yahav E. and Ramalingam G. December 2003[access paper] (revised version appeared in PLDI 2004) |
| Shallow Finite State Verification, Field J., Goyal D., Ramalingam G., and Yahav E. November 2002 [ps][pdf] (revised version appeared in SAS 2003) |
| Automatic Verification of Temporal Properties of Concurrent Heap-Manipulating
Programs using Evolution Logic Yahav E., Reps T., Sagiv M. 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. Yahav E., Reps T., and Sagiv M. 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 Yahav E. 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) |