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
 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). |