Journal Publications

  • Characterizing Transactional Memory Consistency Conditions using Observational Refinement
    Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
    Accepted on 2/Aug/2017 to JACM: Journal of the ACM.
  • Property-Directed Inference of Universal Invariants or Proving Their Absence
    Alexander Karbyshev, Nikolaj Bjorner, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham
    JACM: Journal of the ACM, Volume 64 Issue 1, March 2017.
    [pdf] [bib]
  • 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

  • Statistical Reconstruction of Class Hierarchies in Binaries
    Omer Katz, Noam Rinetzky, Eran Yahav.
    ASPLOS'18: The 23rd ACM International Conference on Architectural Support for Programming Languages and Operating Systems. Williamsburg, VA, USA.
    [bib]
  • Online Detection of E ectively Callback Free Objects with Applications to Smart Contracts
    Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar.
    POPL'18: The 45th ACM SIGPLAN Symposium on Principles of Programming Languages. Los Angeles, CA, United States. (CC)
    [bib] [pdf]
  • RATCOP: Relational Analysis Tool for Concurrent Programs (tool paper)
    Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza and Noam Rinetzky.
    HVC'17: 13th Haifa Verification Conference.
    [bib] [pdf]
  • Thread-Local Semantics and its Efficient Sequential Abstractions for Race-Free Programs
    Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza and Noam Rinetzky.
    SAS'17: 22nd International Static Analysis Symposium. © Springer-Verlag
    (Suvam Mukherjee and Oded Padon were awarded the Radhia Cousot Young Researcher Best Paper Award.) [bib] [pdf]
  • Verifying Equivalence of Spark Programs
    Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, and Mooly Sagiv.
    CAV'17: Conference on Computer Aided Verification. © Springer-Verlag
    [bib] [pdf] [Slides]
  • On the automated verification of web applications with embedded SQL
    Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith and Florian Zuleger.
    ICDT'17: International Conference on Database Theory.
    [bib] [pdf]
  • Conjunctive Abstract Interpretation using Paramodulation
    Or Ozeri, Oded Padon, Noam Rinetzky, and Mooly Sagiv.
    VMCAI'17: International Conference on Verification, Model Checking, and Abstract Interpretation. © Springer-Verlag
    [bib] [pdf]
  • From Shape Analysis to Termination Analysis in Linear Time Roman Manevich, Boris Dogadov, and Noam Rinetzky. CAV'16: Conference on Computer Aided Verification, Toronto, Ontario, Canada, July 2016. © Springer-Verlag
    [bib] [pdf] [Slides] (Slides by Roman Manevich)
  • Property Directed Abstract Interpretation
    Noam Rinetzky and Sharon Shoham
    VMCAI'16: International Conference on Verification, Model Checking, and Abstract Interpretation. January 17-19, 2016, St. Petersburg, Florida, United States. © Springer-Verlag (Best paper award.)
    [bib] [pdf] [Slides]
  • A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms
    Orr Tamir, Adam Morrison, and Noam Rinetzky
    OPODIS'15: International Conference on Principles of Distributed Systems. December 14-17, 2015, Rennes, France.
    [bib] [pdf]
  • Modular Verification of Concurrency-Aware Linearizability
    Nir Hemed, Noam Rinetzky, and Viktor Vafeiadis
    DISC'15: 29th Symposium on Distributed Computing. October 5-9, 2015, Tokyo, Japan. © Springer-Verlag
    [bib] [pdf] [Thesis]
  • Modularity in Lattices: A Case Study on the Correspondence between Top-Down and Bottom-Up Analysis
    Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Mooly Sagiv, and Hongseok Yang
    SAS'15: 22nd International Static Analysis Symposium, Saint-Malo, France, September 9-11, 2015. © Springer-Verlag
    [bib] [pdf] [slides (pptx)] [slides (pdf)]
  • Pattern-based Synthesis of Synchronization for the C++ Memory Model
    Yuri Meshman, Noam Rinetzky, and Eran Yahav
    FMCAD'15: Formal Methods in Computer-Aided Design, September 27-30, 2015, Austin, Texas, USA © FMCAD Inc.
    [bib] [pdf]
  • Property-Directed Inference of Universal Invariants or Proving Their Absence
    Alexander Karbyshev, Nikolaj Bjorner, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham
    CAV'15: 27th International Conference on Computer Aided Verification, July 18-24, 2015, San Francisco, California. © Springer-Verlag
    [bib] [pdf]
  • Safety of Live Transactions in Transactional Memory: TMS is Necessary and Sufficient
    Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
    DISC'14: International Symposium on Distributed Computing. Austin, Texas, USA. ACM, 2014. © Springer-Verlag
    [bib] [pdf]
  • Brief Announcement: Concurrency-Aware Linearizability
    Nir Hemed and Noam Rinetzky
    PODC'14: Symposium on Principles of Distributed Computing, Paris, France. ACM, 2014. © ACM, (2010)
    [bib] [pdf]
  • Tightfit: Adaptive Parallelization with Foresight
    Omer Tripp and Noam Rinetzky
    ESEC/FSE'13: Conference on the Foundations of Software Engineerinq. Saint Petersburg, Russia. ACM, 2013. © ACM, (2010)
    [bib] [pdf] [tr] [slides]
  • A Programming Language Perspective on Transactional Memory Consistency
    Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
    PODC'13: Symposium on Principles of Distributed Computing, Montreal, Canada. ACM, 2013. © ACM, (2010)
    [bib] [pdf] [tr]
  • Verifying Concurrent Memory Reclamation Algorithms with Grace
    A. Gotsman, N. Rinetzky and H. Yang
    ESOP '13: 22nd European Symposium on Programming (ESOP), Rome, Italy, March 16-24, 2013. © Springer-Verlag
    [bib] [pdf] [tr]
  • Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs
    J. Kreiker, T. Reps, N. Rinetzky, M. Sagiv, R. Wilhelm, and E. Yahav
    LNCS 7797: Speacial issue commemorating Harald Ganzinger. 2013. © Springer-Verlag
    [bib] [pdf] [tr]
  • 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

  • Safety of Live Transactions in Transactional Memory: TMS is Necessary and Sufficient
    Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
    WTTM'14: 6th Workshop on the Theory of Transactional Memory EuroTM. Paris, France, 2014.
    [bib] [pdf]
  • 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 veriļ¬cation 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

  • 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

  • Verifying Equivalence of Spark Programs
    Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, and Mooly Sagiv
    Technical Report, School of Computer Science, Tel Aviv University, 2016 (under submission)
    [bib] [pdf]
  • Modular Lattices for Compositional Interprocedural Analysis
    G. Castelnuovo, M. Naik, N. Rinetzky, M. Sagiv, and H. Yang
    TR-103/13, School of Computer Science, Tel Aviv University, 2013
    [bib] [pdf]
  • 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]