Verification via Structure Simulation. - Neil Immerman; Alexander Moshe Rabinovich; Thomas W. Reps; Shmuel Sagiv; Greta Yorsh (CAV, 2004)

The Boundary Between Decidability and Undecidability for Transitive-Closure Logics. - Neil Immerman; Alexander Moshe Rabinovich; Thomas W. Reps; Shmuel Sagiv; Greta Yorsh (CSL, 2004)

Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. - Greta Yorsh; Thomas W. Reps; Shmuel Sagiv (TACAS, 2004)

Symbolic Implementation of the Best Transformer. - Thomas W. Reps; Shmuel Sagiv; Greta Yorsh (VMCAI, 2004)

A Combination Method for Generating Interpolants. - Greta Yorsh; Madanlal Musuvathi (CADE, 2005)

Abstraction for Falsification. - Thomas Ball 001; Orna Kupferman; Greta Yorsh (CAV, 2005)

Automatic Verification of Strongly Dynamic Software Systems. - Nurit Dor; John Field; Denis Gopan; Tal Lev-Ami; Alexey Loginov; Roman Manevich; G. Ramalingam; Thomas W. Reps; Noam Rinetzky; Mooly Sagiv; Reinhard Wilhelm; Eran Yahav; et al. (VSTTE, 2005)

Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs: Ongoing Work. - Greta Yorsh; Alexey Skidanov; Thomas W. Reps; Shmuel Sagiv (AIOOL@VMCAI, 2005)

Testing, abstraction, theorem proving: better together! - Greta Yorsh; Thomas Ball 001; Mooly Sagiv (ISSTA, 2006)

A logic of reachable patterns in linked data-structures. - Greta Yorsh; Alexander Moshe Rabinovich; Mooly Sagiv; Antoine Meyer; Ahmed Bouajjani (J. Log. Algebraic Methods Program., 2007)

Logical characterizations of heap abstractions. - Greta Yorsh; Thomas W. Reps; Mooly Sagiv; Reinhard Wilhelm (ACM Trans. Comput. Log., 2007)

Employing decision procedures for verification of heap-manipulating programs - Greta Yorsh (2007)

Generating precise and concise procedure summaries. - Greta Yorsh; Eran Yahav; Satish Chandra 001 (POPL, 2008)

Experience with Model Checking Linearizability. - Martin T. Vechev; Eran Yahav; Greta Yorsh (SPIN, 2009)

Inferring Synchronization under Limited Observability. - Martin T. Vechev; Eran Yahav; Greta Yorsh (TACAS, 2009)

Simulating reachability using first-order logic with applications to verification of linked data structures - Tal Lev-Ami; Neil Immerman; Thomas W. Reps; Mooly Sagiv; Siddharth Srivastava 001; Greta Yorsh (Log. Methods Comput. Sci., 2009)

PHALANX: parallel checking of expressive heap assertions. - Martin T. Vechev; Eran Yahav; Greta Yorsh (ISMM, 2010)

Verifying linearizability with hindsight. - Peter W. O'Hearn; Noam Rinetzky; Martin T. Vechev; Eran Yahav; Greta Yorsh (PODC, 2010)

Sprint: speculative prefetching of remote data. - Arun Raman; Greta Yorsh; Martin T. Vechev; Eran Yahav (OOPSLA, 2011)

HAWKEYE: effective discovery of dataflow impediments to parallelization. - Omer Tripp; Greta Yorsh; John Field; Mooly Sagiv (OOPSLA, 2011)

Abstraction-guided synthesis of synchronization. - Martin T. Vechev; Eran Yahav; Greta Yorsh (Int. J. Softw. Tools Technol. Transf., 2013)

Unbounded superoptimization. - Abhinav Jangda; Greta Yorsh (Onward!, 2017)