| Verifying Safety Properties Using Separation and Heterogeneous
Abstractions, Yahav E. and Ramalingam G. PLDI 2004 [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 2003 [bib][abstract][ps][pdf][slides] extended version submitted for journal publication |
| Typestate Verification: Abstraction Techniques and Complexity Results,
Field J., Goyal D., Ramalingam G., and Yahav E., SAS 2003 [bib][abstract][ps][pdf][slides] (while in summer internship at IBM T.J. Watson). extended version submitted for journal publication |
| Verifying Temporal Heap Properties Specified via Evolution Logic, Yahav E., Reps T., Sagiv M., and Wilhelm R., ESOP 2003 [bib][abstract][ps][pdf][supplement][slides] |
| Verifying Safety Properties of Concurrent Java Programs using 3-Valued Logic,
Yahav E., POPL 2001 [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). |
| Automatically Verifying Concurrent Queue Algorithms,
Yahav E. and Sagiv M., SoftMC 2003, [bib][abstract][ps][pdf][slides] |
| Automatic Verification of Temporal Heap Properties, Yahav E., Pnueli A., Reps T., and Sagiv M. January 2004, submitted for publication [ps] |
| Generating Concrete Counterexamples for Sound Abstract
Interpretation, Erez G., Yahav E., and Sagiv M., January 2004, submitted for publication [ps] |
| Verifying Safety Properties Using Separation and Heterogeneous
Abstractions, Yahav E. and Ramalingam G. December 2003, [access paper] to appear 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] |
| Solving The Apprentice Challenge with 3VMC [bib][abstract][ps][html][pdf] (original challenge by J. Moore) |
Last Updated: 13/06/04 |
Copyright © 1999, Eran Yahav. |