Greta Yorsh - papers

Publications

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

Master Thesis

Logical characterizations of heap abstractions. gammaHat

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; Defense slides]

Presentations/Talks

Tutorial: Introduction to Separation Logic. [Slides]
Presented at IBM Hawthorne, April 2008.
A Logic of Reachable Patterns in Linked Data-Structures. [Slides].
- Conference talk at FOSSACS 2006.
- Invited talk at HAV workshop, March 2007.
- Computer Laboratory Logic and Semantics Seminar, University of Cambridge, UK, February 2007.
- Research Seminar, Analysis of computer systems (ACSys) group, NYU, October 2007.
- Seminar in Computational Logic, CUNY, September, 2007.
- Semantics and its Applications Workshop, CS-TAU, December 2005.
- Dagstuhl seminar "Software Verification: Infinite-State Model Checking and Static Program Analysis", February 2006.
A Combination Method for Generating Interpolants. [Slides]
- Conference talk at CADE-20, 2005.
Abstraction for Falsification. [Slides]
- Conference talk at CAV 2005.
- Also presentated at MSR Cambridge, June 2005.
Symbolically computing most-precise abstract operations for shape analysis. [Slides]
- Conference talk at TACAS 2004.
- Dagstuhl seminar "Applied Deductive Verification" . November 2003. [Slides]
Symbolic implementation of the best transformer. [Slides]
- Conference talk at VMCAI 2004.
Logical characterizations of heap abstractions.
- Logic seminar at CS-TAU, March 2003. [Slides]
- Dagstuhl seminar "Reasoning about shape", March 2003. [Slides]
Handling trees in TVLA and Improved Focus operation. Miniseminar of TAU Programming Languages Group, Hof Yarok, Natanya, Dec. 2001. [Slides]

Research Internships

2006 - Program Analysis Group, IBM Research, T.J. Watson Research Center, Hawthorne, US
2005 - TVM group , Microsoft Research , Redmond, US
2004 - TVM group , Microsoft Research , Redmond, US

Schools and Seminars

Dagstuhl seminar "Software Verification: Infinite-State Model Checking and Static Program Analysis", February 2006.
Semantics and its Applications Workshop, December 19-20, 2005, Tel Aviv University, Israel.
UW/MSR 2004 Summer Institute on Trends in Testing: Theory, Techniques and Tools, August 22-26, 2004, Portland, Oregon.
Combination of Decision Procedures Summer School, August 9-11, 2004, SRI International.
Minerva Formal-Verification School at Schefaim, Israel, 16-19 May, 2004
Dagstuhl seminar "Applied Deductive Verification" , November 2003.
Dagstuhl seminar "Reasoning about shape", March 2003.
Marktoberdorf Summer School on Models, Algebras, and Logic of Engineering Software. July 30 to August 11, 2002.

Courses

Outdated Resources

A (partial) bibliography on assume-guarantee reasoning of sequantial and multithreaed programs. Collected by Mooly Sagiv, Noam Rinetzky, and Greta Yorsh. Last updated in February 2005.
TVLA
CoreC - a small subset of the C language, which enables faster specification and development of source-code analyzers.
- The design of CoreC [PS; PDF]
- Translation rules from C to CoreC
GFC - Generic Frontend for C. This tool translates C program into different representations, according to user's specifications. GFC was tested as a frontend for TVLA and CSSV applications, and it can be used with other applications as well.
For more information and download, please contact me .
Documentation for the old version of GFC:
- User's Manual for GFC.
- Example use of GFC to generate TVLA input for shape analysis of linked lists [PPT].

In the US, everything that is not prohibited by law is permitted.
In Germany, everything that is not permitted by law is prohibited.
In Russia, everything is prohibited, even if permitted by law.
In Israel, everything is permitted, even if prohibited by law.

Home - Contact - Academic - CV - Fun

Last modified: 2007

Top of Page