Publications

  • Greta Yorsh, Eran Yahav, Martin Vechev, Bard Bloom
    Phalanx: Parallel Checking of Expressive Heap Assertions
    IBM Technical Report RC24822, May 2009
    [Abstract; TR-PDF; TR-PS; Slides]

  • Noam Rinetzky, Martin Vechev, Eran Yahav, Greta Yorsh
    Verifying Optimistic Algorithms Should be Easy (position paper)
    To appear in Exploiting Concurrency Efficiently and Correctly -- EC^2 2009 (CAV 2009 Workshop)
    [PDF; PS]

  • Martin Vechev, Eran Yahav, Greta Yorsh
    Experience with Model Checking Linearizability
    To appear in Proc. SPIN Workshop on Model Checking of Software (SPIN 2009)
    [Abstract; PDF; PS]

  • Martin Vechev, Eran Yahav, Greta Yorsh
    Inferring Synchronization under Limited Observability
    In Proc. Tools and Algorithms for the Construction and Analysis of Systems, 2009 (TACAS 2009)
    [Abstract; PDF; PS; Slides]
    Full version, including proofs, appeared as IBM Technical Report RC24661, October, 2008
    [TR-PDF; TR-PS]

  • Martin Vechev, Eran Yahav, Maged Michael, Hagit Attiya, Greta Yorsh
    Computer-Assisted Construction of Efficient Concurrent Algorithms (position paper)
    Exploiting Concurrency Efficiently and Correctly -- EC^2 2008 (CAV 2008 workshop)
    [PDF;PS]

  • Greta Yorsh, Eran Yahav, and Satish Chandra
    Generating Precise and Concise Procedure Summaries
    In Proc. ACM Symposium on Principles of Programming Languages, 2008 (POPL 2008)
    [Abstract; PDF; PS; Slides (short version - POPL'08 talk); Slides (longer version);]

  • Greta Yorsh, Thomas Ball, Mooly Sagiv,
    Testing, Abstraction, Theorem Proving: Better Together!
    In Proc. International Symposium on Software Testing and Analysis, 2006 (ISSTA 2006)
    [Abstract ; Slides] Full version (including proofs): [PS; PDF]

  • Greta Yorsh, Alexander Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani,
    A Logic of Reachable Patterns in Linked Data-Structures.
    In Proc. Foundations of Software Science and Computation Structures, 2006 (FOSSACS 2006)
    [Abstract; Slides]
    Extended version (including proofs) appears in Journal of Logic and Algebraic Programming:
    [PDF]

  • Greta Yorsh and Madan Musuvathi,
    A Combination Method for Generating Interpolants.
    In Proc. Conf. on Automated Deduction, 2005 (CADE-20, 2005)
    [Abstract; PS; PDF; Slides]
    Microsoft Research Technical Report, MSR-TR-2004-108, October 2004
    [TR-PDF]

  • Tal Lev-Ami, Neil Immerman, Thomas Reps, Mooly Sagiv, Siddharth Srivastava, and Greta Yorsh,
    Simulating reachability using first-order logic with applications to verification of linked data structures.
    In Proc. Conf. on Automated Deduction, 2005 (CADE-20, 2005)

  • Thomas Ball, Orna Kupferman, and Greta Yorsh,
    Abstraction for Falsification.
    In Proc. Computer Aided Verification, 2005 (CAV 2005 )
    [Slides]
    Full version appears as a Microsoft Research Technical Report MSR-TR-2005-50, June 2005
    [MSR-TR]

  • Greta Yorsh, Alexey Skidanov, Thomas Reps and Mooly Sagiv
    Automatic Assume/Guarantee Reasoning for Heap-Manupilating Programs (Ongoing work).
    A short version of this report appears in AIOOL, 2005.
    [ Short version - Abstract and PDF; Full version - PS]

  • Neil Immerman, Alexander Rabinovich, Thomas Reps, Mooly Sagiv and Greta Yorsh,
    The Boundary Between Decidability and Undecidability for Transitive Closure Logics.
    In Proc. Computer Science Logic, 2004 (CSL 2004)

  • Neil Immerman, Alexander Rabinovich, Thomas Reps, Mooly Sagiv and Greta Yorsh,
    Verification via structure simulation.
    In Proc. Computer Aided Verification, 2004 (CAV 2004)
    [Abstract; PS; PDF]

  • Greta Yorsh, Thomas Reps and Mooly Sagiv,
    Symbolically computing most-precise abstract operations for shape analysis.
    In Proc. Tools and Algorithms for the Construction and Analysis of Systems, 2004 (TACAS 2004)
    [Abstract; PS; PDF; Slides]
    Technical Report (including the proofs), School of Computer Sciences, Tel Aviv University, Sept. 2003.
    [PS; PDF]

  • Thomas Reps, Mooly Sagiv and Greta Yorsh,
    Symbolic implementation of the best transformer.
    In Proc. Verification, Model Checking, and Abstract Interpretation, 2004 (VMCAI 2004)
    [Abstract; PS; PDF; Slides]

Theses

  • Employing decision procedures for verification of heap-manipulating programs.
    PhD Thesis, Tel Aviv University. December 2007.
    [PS; PDF; Slides (public lecture on thesis results)]

  • Logical characterizations of heap abstractions.
    Master's Thesis, Tel Aviv University, March 2003.
    • The revised and extended version of the main result of my master thesis published in
      ACM Transactions on Computational Logic (TOCL), January 2007.
      [PS; PDF]
    • Spass input files used to verify the examples in the paper [SPASSInputs.zip]
    • A note comparing this work with a recent related work.
    • The original version, including "The design of CoreC" in the Appendix, March 2003.
      [PS; PDF; Slides (defense)]

Disclaimer

This web page contains links to PS and PDF files of articles that may be covered by copyright. You may browse the articles at your convenience. Retrieving, copying, or distributing these files may violate copyright law. The files are provided here as a courtesy, and, in some cases, there may be differences between the version provided here and the published version. If you cite these articles, please cite the published version rather than giving a URL.