Journal Publications

  • Characterizing Transactional Memory Consistency Conditions using Observational Refinement
    Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
    JACM: Journal of the ACM, Volume 65, Number 1. Publication date: December 2017.
    [pdf] [bib]
  • 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. Publication date: 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

  • Hypothetical Reasoning via Provenance Abstraction
    Daniel Deutch, Yuval Moskovitch and Noam Rinetzky.
    SIGMOD'19: ACM SIGMOD International Conference on Management of Data.
    June 30 - July 5, 2019 - Amsterdam, The Netherlands.
    [bib]
  • Order out of Chaos: Proving Linearizability Using Local Views
    Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky and Sharon Shoham.
    DISC'18: The 32nd International Symposium on DIStributed Computing.
    October 15-19, 2018 - New Orleans, Louisiana.
    [bib] [TR]
  • Short Paper: Towards Hypothetical Reasoning using Distributed Provenance
    Daniel Deutch, Yuval Moskovitch, Itay Polack Gadassi and Noam Rinetzky.
    EDBT'18: The 21st International Conference on Extending Database Technology.
    March 26-29, 2018 - Vienna, Austria.
    [bib] [pdf]
  • Chopped symbolic execution
    David Trabish, Andrea Mattavelli, Noam Rinetzky and Cristian Cadar.
    ICSE'18: The 40th International Conference on Software Engineering.
    May 27 - 3 June 2018 - Gothenburg, Sweden.
    [bib] [pdf] [Slides] [software]
  • Safe Privatization in Transactional Memory
    Artem Khyzha, Hagit Attiya, Alexey Gotsman and Noam Rinetzky.
    PPoPP'18: The 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming.
    February 24-28, 2018 - Vösendorf / Wien, Austria.
    [bib] [pdf]
  • Statistical Reconstruction of Class Hierarchies in Binaries
    Omer Katz, Noam Rinetzky and Eran Yahav.
    ASPLOS'18: The 23rd ACM International Conference on Architectural Support for Programming Languages and Operating Systems.
    January 7-13, 2018 - Williamsburg, VA, USA.
    [bib] [pdf]
  • Online Detection of Effectively 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.
    [bib] [pdf] [Slides] [TR] [Code] [©CC]
  • 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.
    November 13-15, 2017 - Haifa, Israel.
    [bib] [pdf] [© Springer-Verlag]
  • 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.
    August 30 - September 1, 2017 - New York, NY, USA
    (Suvam Mukherjee and Oded Padon were awarded the Radhia Cousot Young Researcher Best Paper Award.)
    [bib] [pdf] [© Springer-Verlag]
  • Verifying Equivalence of Spark Programs
    Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, and Mooly Sagiv.
    CAV'17: Conference on Computer Aided Verification.
    July 24-28, 2017 - Heidelberg, Germany
    [bib] [pdf] [Slides] [© Springer-Verlag]
  • 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.
    March 21-24, 2017 - Venice, Italy
    [bib] [pdf] [©CC]
  • 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.
    January 15-17, 2017, Paris, France
    [bib] [pdf] [© Springer-Verlag]
  • From Shape Analysis to Termination Analysis in Linear Time
    Roman Manevich, Boris Dogadov, and Noam Rinetzky.
    CAV'16: Conference on Computer Aided Verification.
    July, 2016 - Toronto, Ontario, Canada.
    [bib] [pdf] [Slides] [© Springer-Verlag]
  • 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.
    (Best paper award.)
    [bib] [pdf] [Slides] [© Springer-Verlag]
  • 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] [©CC]
  • 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.
    [bib] [pdf] [Thesis] [© Springer-Verlag]
  • 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.
    [bib] [pdf] [slides (pptx)] [slides (pdf)] [© Springer-Verlag]
  • 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.
    [bib] [pdf] [© FMCAD Inc.]
  • 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.
    [bib] [pdf] [© Springer-Verlag]
  • 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.
    [bib] [pdf] [© Springer-Verlag]
  • Brief Announcement: Concurrency-Aware Linearizability
    Nir Hemed and Noam Rinetzky
    PODC'14: Symposium on Principles of Distributed Computing.
    Paris, France. ACM, 2014.
    [bib] [pdf] [© ACM]
  • Tightfit: Adaptive Parallelization with Foresight
    Omer Tripp and Noam Rinetzky
    ESEC/FSE'13: ACM SIGSOFT Conference on the Foundations of Software Engineering.
    August 18-26, 2013 - Saint Petersburg, Russia.
    [bib] [pdf] [tr] [slides] [© ACM]
  • A Programming Language Perspective on Transactional Memory Consistency
    Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky
    PODC'13: ACM Symposium on Principles of Distributed Computing.
    July 22-24, 2013 - Montreal, Canada.
    [bib] [pdf] [tr] [© ACM]
  • Verifying Concurrent Memory Reclamation Algorithms with Grace
    A. Gotsman, N. Rinetzky and H. Yang
    ESOP '13: 22nd European Symposium on Programming.
    March 16-24, 2013 - Rome, Italy.
    [bib] [pdf] [tr] [© Springer-Verlag]
  • 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
    [bib] [pdf] [tr] [© Springer-Verlag]
  • 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
    [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.
    January 20-22, 2010 - Madrid, Spain.
    [bib] [pdf] [tr bib] [tr pdf] [slides] [© ACM]
  • 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 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

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