Noam Rinetzky

Publications

Journal Publications

• Abstraction for concurrent objects
  I. Filipovic, P. O'Hearn, N. Rinetzky, and H. Yang.
  TCS: Theoretical Computer Science, 2010. © Elsevier B.V.
  [bib] [pdf] [slides]
• On the complexity of partially-flow-sensitive alias analysis
  N. Rinetzky, G. Ramalingam, M. Sagiv, and E. Yahav
  TOPLAS: ACM Transactions on Programming Languages and Systems. 30(3): 13:1-13:28, May 2008. © ACM
  [bib] [pdf]

Conference Publications

• Field-Sensitive Program Dependence Analysis
  S. Litvak, N. Dor, R. Bodik, N. Rinetzky, and M. Sagiv
  FSE '10: ACM SIGSOFT 18th International Symposium on the Foundations of Software Engineering, Santa Fe, New Mexico, USA, November 7-11, 2010. © ACM, (2010)
  [bib] [pdf] [slides]
• Verifying Linearizability with Hindsight
  P. W. O'Hearn, N. Rinetzky, M. T. Vechev, E. Yahav, and G. Yorsh
  PODC '10: 29th Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, Zurich, Switzerland, July 25-28, 2010. © ACM, (2010)
  [bib] [pdf] [slides] [Technical report available upon request]
• Sequential verification of serializability
  H. Attiya, G. Ramalingam, and N. Rinetzky
  POPL '10: 37nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Madrid, Spain, January 20-22, 2010. © ACM, (2010)
  [bib] [pdf] [tr bib] [tr pdf] [slides]
• Abstraction for Concurrent Objects
  Ivana Filipovic, Peter O'Hearn, Noam Rinetzky, Hongseok Yang
  ESOP '09: 18th European Symposium on Programming. York, United Kingdom, March 25-27, 2009. © Springer-Verlag
  [bib] [pdf] [journal version] [slides]
• Verifying dereference safety via expanding-scope analysis
  A. Loginov , E. Yahav , S. Chandra , S. Fink , N. Rinetzky , M. G. Nanda
  ISSTA '08: International Symposium on Software Testing and Analysis. © ACM, (2008)
  [bib] [pdf]
  
• Local reasoning for storable locks and threads
  A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv.
  APLAS'07: The Fifth ASIAN Symposium on Programming Languages and Systems. Pages 19-37. © Springer-Verlag
  [bib] [pdf] [tr pdf]
• Comparison under abstraction for verifying linearizability
  D. Amit, N. Rinetzky, T. Reps, M. Sagiv, and E. Yahav
  CAV '07: 19th International Conference on Computer Aided Verification, pages: 477-490. © Springer-Verlag
  [bib] [pdf] [ps] [D. Amit's MsC thesis] [slides]
• CGCExplorer: A semi-automated search procedure for provably correct concurrent collectors
  M. Vechev, E. Yahav, D.F. Bacon, and N.Rinetzky
  PLDI '07: ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pages:456-467. © ACM, (2007)
  [bib] [pdf] [ps] [slides]
• Modular shape analysis for dynamically encapsulated programs
  N. Rinetzky, A. Poetzsch-Heffter, G. Ramalingam, M. Sagiv, and E. Yahav
  ESOP '07: 16th European Symposium on Programming, Braga (Portugal), 24 March - 1 April, 2007, pages:220-236. © Springer-Verlag
  [bib] [pdf] [ps] [ppt]
  Technical Report (TAU-CS-107/06): [tr pdf] [tr ps]
• Interprocedural shape analysis for cutpoint-free programs
  N. Rinetzky, M. Sagiv, and E. Yahav
  SAS '05: 12th International Static Analysis Symposium, London, September 7-9, 2005, pages:284-302. © Springer-Verlag
  [bib] [pdf] [ps] [tr pdf] [tr ps] [slides]
• A semantics for procedure local heaps and its abstractions
  N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm
  POPL '05: 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Long Beach, California, January 12-14, 2005, pages: 296-309. © ACM, (2005)
  [bib] [pdf] [ps] [tr pdf] [tr ps] [slides]
• Interprocedural shape analysis for recursive programs
  N. Rinetzky and M. Sagiv
  CC '01: Compiler Construction, 10th International Conference, CC 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, pages: 133-149. © Springer-Verlag
  [bib] [pdf] [MsC] [slides]

Workshop Publications

• Verifying optimistic algorithms should be easy (position paper)
  N. Rinetzky, M. T. Vechev, E. Yahav, and G. Yorsh
  EC2 '09: Exploiting Concurrency Efficiently and Correctly - (EC)2. CAV 2009 Workshop, June 26-27, 2009, Grenoble, France
  [bib] [pdf] [slides]
• Modular verification with shared abstractions
  J. Juhasz, N. Rinetzky, A. Poetzsch-Heffter, M. Sagiv, and E. Yahav
  FOOL '09: 2009 International Workshop on Foundations of Object-Oriented Languages (FOOL'09). Saturday, 24 January 2009 Savannah, Georgia, USA
  [bib] [pdf] [slides]

Miscellaneous Publications

• Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs
  J. Kreiker, T. Reps, N. Rinetzky, M. Sagiv, R. Wilhelm, and E. Yahav
  LNCS speacial issue commemorating Harald Ganzinger. (To be published.)
  [bib] [pdf]
• Automatic verification of strongly dynamic software systems
  N. Dor, J. Field, D. Gopan, T. Lev-Ami, A. Loginov, R. Manevich, G. Ramalingam, T. Reps, N. Rinetzky, M. Sagiv, R. Wilhelm, E. Yahav, G. Yorsh
  VSTTE '03: In Proc. IFIP working conference on verified software: Theories, Tools, Experiments, Zurich, Switzerland, Oct.10-13, 2005. [bib] [pdf]
• Towards an object store
  A. Azagury, V. Dreizin, M. Factor, E. Henis, D. Naor, N. Rinetzky, O. Rodeh, J. Satran, A. Tavory, and L. Yerushalmi
  MSS '03: 20th IEEE/11th NASA Goddard Conference on Mass Storage Systems and Technologies, April 7-10, 2003, San Diego, California, USA, pages: 165--176. © IEEE, (2003)
  [bib] [pdf]
• A Two-layered approach for securing an object store network
  A. Azagury, R. Canetti, M. Factor, S. Halevi, E. Henis, D. Naor, N. Rinetzky, O. Rodeh, and J. Satran
  SISW '02: 1st International IEEE Security in Storage Workshop, Greenbelt, Maryland, USA, Greenbelt, Maryland, USA, pages: 10--23. © IEEE, (2002)
  [bib] [pdf]

Technical Reports

• Resilient verification for optimistic concurrent algorithms
  N. Rinetzky, P. W. O'Hearn, M. T. Vechev, E. Yahav, and G. Yorsh
  Department of Computer Science, Queen Mary University of London, July 2009
  Superseded by newer work: "Verifying Linearizability with Hindsight". TR available upon request.
• Componentized heap abstraction
  N. Rinetzky, G. Ramalingam, E. Yahav, and M. Sagiv
  TR-164/06, School of Computer Science, Tel Aviv University, December 2006
  [bib] [pdf]
• Interprocedural functional shape analysis using local heaps
  N. Rinetzky, M. Sagiv, and E. Yahav
  TR-26/04, School of Computer Science, Tel Aviv University, November 2004
  [bib] [pdf] [ps]

Manuscripts

• PhD Dissertation: Interprocedural and modular local heap shape analysis
  Noam Rinetzky
  Tel Aviv University
  Submitted June 2008. Approved January 2009
  [bib] [pdf]
• MSc Thesis: Interprocedural shape analysis
  Noam Rinetzky
  Technion Israel Institute of Technology
  Submitted December 2000. Approved 2001
  [bib] [pdf]