Publications By Year [Show By Topic]
Conferences
| Abstraction-Guided Synthesis Vechev M., Yahav E., Yorsh G. POPL '10: 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages [bib] [abstract] [pdf] [slides] to appear |
| 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] |
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. 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] |
| 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] |
| 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] |
| 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] extended version accepted for journal publication |
| Typestate Verification: Abstraction Techniques and Complexity Results,
Field J., Goyal D., Ramalingam G., and Yahav E., SAS '03 [bib] [abstract] [ps] [pdf] [slides] extended version accepted for journal publication |
| 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] |
| 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). |
Journals
| Static Specification Mining Using Automata-Based Abstractions Shoham S., Yahav E., Fink S., Pistoia M. IEEE Transactions on Software Engineering (TSE 2008). |
|
| 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 (TOSEM 2008). | |
| 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). | |
| 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 | |
| Verifying Temporal Heap Properties Specified via Evolution Logic
E. Yahav, T. Reps, M. Sagiv, and R. Wilhelm Logic Journal of IGPL, September 2006 |
|
| 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 |
Workshops
| 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] |
| Cartesian Partial-Order Reduction Gueta G., Flanagan C., Yahav E., and Sagiv M. SPIN '07: 14th Workshop on Model Checking Software [bib][abstract][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] |
| Automatically Verifying Concurrent Queue Algorithms,
Yahav E. and Sagiv M., SoftMC 2003: Workshop on Software Model Checking [bib][abstract][ps][pdf][slides] |
Position Papers
| 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] |
| 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] |
Technical Reports
| 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] |
| Symbolic Summarization with Applications to Typestate Verification Yorsh G., Yahav E., and Chandra S. [pdf] |
| When Role Models Have Flaws: Static Validation of Enterprise Security Policies Pistoia M., Fink S.J., Flynn R.J., Yahav E. September 2006,[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] |
| 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) |