≈ ÷ Greta Yorsh - Publications

Publications

  • Abhinav Jangda and Greta Yorsh
    Unbounded Superoptimization.
    In ACM Symposium on New Ideas in Programming and Reflections on Software, 2017 (Onward! 2017)
    [PDF; Slides]

  • Omer Tripp, Greta Yorsh, John Field, Mooly Sagiv
    HAWKEYE: Effective Discovery of Dataflow Impediments to Parallelization.
    In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2011 (OOPSLA'11)
    [Abstract; PDF]

  • Arun Raman, Greta Yorsh, Martin T. Vechev, Eran Yahav
    Sprint: Speculative Prefetching of Remote Data.
    In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2011 (OOPSLA'11)
    [Abstract; PDF]

  • Martin Vechev, Eran Yahav, Greta Yorsh
    Abstraction-Guided Synthesis of Synchronization
    In Proc. ACM Symposium on Principles of Programming Languages, 2010 (POPL'10)
    [Abstract; PDF; PS]

  • Martin Vechev, Eran Yahav, Greta Yorsh,
    Phalanx: Parallel Checking of Expressive Heap Assertions
    In Proc. International Symposium on Memory Management, 2010 (ISMM'10)
    Full version appears as IBM Technical Report RC24822, May 2009
    [Abstract; PDF; PS; TR-PDF; TR-PS; Slides]

  • Noam Rinetzky, Peter O'Hearn, Martin Vechev, Eran Yahav, Greta Yorsh
    Verifying Linearizability with Hindsight
    In Proc. Principles of Distributed Computing, 2010 (PODC'10)
    [Abstract]
    Preliminary version appears as:
    Verifying Optimistic Algorithms Should be Easy (position paper)
    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
    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, appears 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
    [MSR-TR-PDF]
    Unfortunately, the technical report published by MSR is no longer available.
    The proofs (dated October 2004) can be found in the appendix of this document
    [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)
    In Logical Methods in Computer Science, Volume 5(2), 2009 (LMCS 2009)
    [Journal version]

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