Journal Publications

  • Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules with Callbacks
    Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodriguez-Nunez, Albert Rubio, Mooly Sagiv
    IEEE Transactions on Dependable and Secure Computing, vol. 20, no. 3, pp. 2256-2273, 1 May-June 2023.
    [pdf]
  • Runtime Complexity Bounds Using Squeezers
    Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham
    ACM Transactions on Programming Languages and Systems, Vol. 44, No. 3, Article 17. Publication date: July 2022.
    [pdf]
  • Shape Analysis
    Bor-Yuh Evan Chang, Cezara Dragoi, Roman Manevich, Noam Rinetzky, Xavier Rival
    Foundations and Trends in Programming Languages. Volume 6. No. 1-2. pp. 1-158. 2020.
    [bib] [pdf]
  • 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.
    [bib] [pdf]
  • 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.
    [bib] [pdf]
  • 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 and Workshop Publications

  • State Merging with Quantifiers in Symbolic Execution
    David Trabish, Noam Rinetzky, Sharon Shoham and Vaibhav Sharma.
    ESEC/SIGSOFT FSE 2023: ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. pp 1140-1152.
    [pdf]
  • A Bounded Symbolic-Size Model for Symbolic Execution
    David Trabish, Shachar Itzhaky and Noam Rinetzky.
    ESEC/SIGSOFT FSE 2021: ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering.
    [pdf]
  • Address-Aware Query Caching for Symbolic Execution
    David Trabish, Shachar Itzhaky and Noam Rinetzky.
    ICST 2021: IEEE International Conference on Software Testing, Verification and Validation.
    [pdf]
  • Run-time Complexity Bounds Using Squeezers
    Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham.
    ESOP 2021: European Symposium on Programming.
    [pdf]
  • Past-sensitive pointer analysis for symbolic execution
    David Trabish, Timotej Kapus, Noam Rinetzky, Cristian Cadar.
    ESEC/SIGSOFT FSE 2020: ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 197-208
    [pdf]
  • Proving highly-concurrent traversals correct
    Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham.
    Proc. ACM Program. Lang. 4(OOPSLA): 128:1-128:29 (2020)
    [pdf]
  • Taming callbacks for smart contract modularity
    Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, Mooly Sagiv.
    Proc. ACM Program. Lang. 4(OOPSLA): 209:1-209:30 (2020)
    [pdf]
  • Relocatable addressing model for symbolic execution
    David Trabish, Noam Rinetzky.
    ISSTA 2020: 51-62
    [pdf]
  • Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation
    Oren Ish-Shalom, Shachar Itzhaky, Roman Manevich, Noam Rinetzky.
    VMCAI'20: VMCAI 2020 - 21st International Conference on Verification, Model Checking, and Abstract Interpretation.
    Sun 19 - Sat 25 January 2020. New Orleans, Louisiana, United States.
    [pdf]
  • Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
    Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham.
    VMCAI'20: VMCAI 2020 - 21st International Conference on Verification, Model Checking, and Abstract Interpretation.
    Sun 19 - Sat 25 January 2020. New Orleans, Louisiana, United States.
    [pdf]
  • Computing Summaries of String Loops in C for Better Testing and Refactoring
    Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky and Cristian Cadar.
    PLDI'19: ACM SIGPLAN Conference on Programming Language Design and Implementation.
    22 - 26, 2019 - Phonenix, Arizona, United States.
    [pdf]
  • Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions
    Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk and Mooly Sagiv
    PLDI'19: ACM SIGPLAN Conference on Programming Language Design and Implementation.
    22 - 26, 2019 - Phonenix, Arizona, United States.
    [pdf]
  • COBRA: Compression via Abstraction of Provenance for Hypothetical Reasoning (Demo Paper)
    Daniel Deutch, Yuval Moskovitch and Noam Rinetzky.
    ICDE'19: The 35th IEEE International Conference on Data Engineering.
    April 8 - 12, 2019 - MACAU SAR, China.
    [pdf]
  • 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] [pdf]
  • 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] [pdf] [TR] [slides]
  • 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]
  • 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]
  • 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]
  • 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]
  • 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]
  • 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]
  • 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]
  • 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]

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]