Interprocedural Shape Analysis for Recursive Programs. - Noam Rinetzky; Shmuel Sagiv (CC, 2001)

A Two Layered Approach for Securing an Object Store Network. - Alain Azagury; Ran Canetti; Michael Factor; Shai Halevi; Ealan Henis; Dalit Naor; Noam Rinetzky; Ohad Rodeh; Julian Satran (IEEE Security in Storage Workshop, 2002)

Towards an Object Stor. - Alain Azagury; Vladimir Dreizin; Michael Factor; Ealan Henis; Dalit Naor; Noam Rinetzky; Ohad Rodeh; Julian Satran; Ami Tavory; Lena Yerushalmi (IEEE Symposium on Mass Storage Systems, 2003)

A semantics for procedure local heaps and its abstractions. - Noam Rinetzky; Jörg Bauer 001; Thomas W. Reps; Shmuel Sagiv; Reinhard Wilhelm (POPL, 2005)

Interprocedural Shape Analysis for Cutpoint-Free Programs. - Noam Rinetzky; Mooly Sagiv; Eran Yahav (SAS, 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)

Local Reasoning for Storable Locks and Threads. - Alexey Gotsman; Josh Berdine; Byron Cook; Noam Rinetzky; Mooly Sagiv (APLAS, 2007)

Comparison Under Abstraction for Verifying Linearizability. - Daphna Amit; Noam Rinetzky; Thomas W. Reps; Mooly Sagiv; Eran Yahav (CAV, 2007)

Modular Shape Analysis for Dynamically Encapsulated Programs. - Noam Rinetzky; Arnd Poetzsch-Heffter; Ganesan Ramalingam; Mooly Sagiv; Eran Yahav (ESOP, 2007)

CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors. - Martin T. Vechev; Eran Yahav; David F. Bacon; Noam Rinetzky (PLDI, 2007)

Verifying dereference safety via expanding-scope analysis. - Alexey Loginov; Eran Yahav; Satish Chandra 001; Stephen Fink; Noam Rinetzky; Mangala Gowri Nanda (ISSTA, 2008)

On the complexity of partially-flow-sensitive alias analysis. - Noam Rinetzky; G. Ramalingam; Shmuel Sagiv; Eran Yahav (ACM Trans. Program. Lang. Syst., 2008)

Interprocedural and modular local heap shape analysis - Noam Rinetzky (2008)

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

Sequential verification of serializability. - Hagit Attiya; G. Ramalingam; Noam Rinetzky (POPL, 2010)

Field-sensitive program dependence analysis. - Shay Litvak; Nurit Dor; Rastislav Bodík; Noam Rinetzky; Mooly Sagiv (SIGSOFT FSE, 2010)

Abstraction for concurrent objects. - Ivana Filipovic; Peter W. O'Hearn; Noam Rinetzky; Hongseok Yang (Theor. Comput. Sci., 2010)

Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs. - Jörg Kreiker; Thomas W. Reps; Noam Rinetzky; Mooly Sagiv; Reinhard Wilhelm; Eran Yahav (Programming Logics, 2013)

Verifying Concurrent Memory Reclamation Algorithms with Grace. - Alexey Gotsman; Noam Rinetzky; Hongseok Yang (ESOP, 2013)

A programming language perspective on transactional memory consistency. - Hagit Attiya; Alexey Gotsman; Sandeep Hans; Noam Rinetzky (PODC, 2013)

Tightfit: adaptive parallelization with foresight. - Omer Tripp; Noam Rinetzky (ESEC/SIGSOFT FSE, 2013)

Brief announcement: concurrency-aware linearizability. - Nir Hemed; Noam Rinetzky (PODC, 2014)

Safety of Live Transactions in Transactional Memory: TMS is Necessary and Sufficient. - Hagit Attiya; Alexey Gotsman; Sandeep Hans; Noam Rinetzky (DISC, 2014)

Pattern-based Synthesis of Synchronization for the C++ Memory Model. - Yuri Meshman; Noam Rinetzky; Eran Yahav (FMCAD, 2015)

A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms. - Orr Tamir; Adam Morrison 001; Noam Rinetzky (OPODIS, 2015)

Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis. - Ghila Castelnuovo; Mayur Naik; Noam Rinetzky; Mooly Sagiv; Hongseok Yang (SAS, 2015)

Modular Verification of Concurrency-Aware Linearizability. - Nir Hemed; Noam Rinetzky; Viktor Vafeiadis (DISC, 2015)

From Shape Analysis to Termination Analysis in Linear Time. - Roman Manevich; Boris Dogadov; Noam Rinetzky (CAV (1), 2016)

Property Directed Abstract Interpretation. - Noam Rinetzky; Sharon Shoham (VMCAI, 2016)

Verifying Equivalence of Spark Programs. - Shelly Grossman; Sara Cohen; Shachar Itzhaky; Noam Rinetzky; Mooly Sagiv (CAV (2), 2017)

RATCOP: Relational Analysis Tool for Concurrent Programs. - Suvam Mukherjee; Oded Padon; Sharon Shoham; Deepak D'Souza; Noam Rinetzky (Haifa Verification Conference, 2017)

On the Automated Verification of Web Applications with Embedded SQL. - Shachar Itzhaky; Tomer Kotek; Noam Rinetzky; Mooly Sagiv; Orr Tamir; Helmut Veith; Florian Zuleger (ICDT, 2017)

Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs. - Suvam Mukherjee; Oded Padon; Sharon Shoham; Deepak D'Souza; Noam Rinetzky (SAS, 2017)

Conjunctive Abstract Interpretation Using Paramodulation. - Or Ozeri; Oded Padon; Noam Rinetzky; Mooly Sagiv (VMCAI, 2017)

Property-Directed Inference of Universal Invariants or Proving Their Absence. - Aleksandr Karbyshev; Nikolaj S. Bjørner; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (J. ACM, 2017)

Statistical Reconstruction of Class Hierarchies in Binaries. - Omer Katz; Noam Rinetzky; Eran Yahav (ASPLOS, 2018)

Towards Hypothetical Reasoning Using Distributed Provenance. - Daniel Deutch; Yuval Moskovitch; Itay Polak; Noam Rinetzky (EDBT, 2018)

Chopped symbolic execution. - David Trabish; Andrea Mattavelli; Noam Rinetzky; Cristian Cadar (ICSE, 2018)

Safe privatization in transactional memory. - Artem Khyzha; Hagit Attiya; Alexey Gotsman; Noam Rinetzky (PPoPP, 2018)

Order out of Chaos: Proving Linearizability Using Local Views. - Yotam M. Y. Feldman; Constantin Enea; Adam Morrison 001; Noam Rinetzky; Sharon Shoham (DISC, 2018)

Characterizing Transactional Memory Consistency Conditions Using Observational Refinement. - Hagit Attiya; Alexey Gotsman; Sandeep Hans; Noam Rinetzky (J. ACM, 2018)

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; Yoni Zohar (Proc. ACM Program. Lang., 2018)

COBRA: Compression Via Abstraction of Provenance for Hypothetical Reasoning. - Daniel Deutch; Yuval Moskovitch; Noam Rinetzky (ICDE, 2019)

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; Mooly Sagiv (PLDI, 2019)

Computing summaries of string loops in C for better testing and refactoring. - Timotej Kapus; Oren Ish-Shalom; Shachar Itzhaky; Noam Rinetzky; Cristian Cadar (PLDI, 2019)

Hypothetical Reasoning via Provenance Abstraction. - Daniel Deutch; Yuval Moskovitch; Noam Rinetzky (SIGMOD Conference, 2019)

Relocatable addressing model for symbolic execution. - David Trabish; Noam Rinetzky (ISSTA, 2020)

Past-sensitive pointer analysis for symbolic execution. - David Trabish; Timotej Kapus; Noam Rinetzky; Cristian Cadar (ESEC/SIGSOFT FSE, 2020)

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, 2020)

Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction. - Oren Ish-Shalom; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (VMCAI, 2020)

A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs. - Suvam Mukherjee; Oded Padon; Sharon Shoham; Deepak D'Souza; Noam Rinetzky (CoRR, 2020)

Shape Analysis. - Bor-Yuh Evan Chang; Cezara Dragoi; Roman Manevich; Noam Rinetzky; Xavier Rival (Found. Trends Program. Lang., 2020)

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., 2020)

Proving highly-concurrent traversals correct. - Yotam M. Y. Feldman; Artem Khyzha; Constantin Enea; Adam Morrison 001; Aleksandar Nanevski; Noam Rinetzky; Sharon Shoham (Proc. ACM Program. Lang., 2020)

Run-time Complexity Bounds Using Squeezers. - Oren Ish-Shalom; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (ESOP, 2021)

Address-Aware Query Caching for Symbolic Execution. - David Trabish; Shachar Itzhaky; Noam Rinetzky (ICST, 2021)

A bounded symbolic-size model for symbolic execution. - David Trabish; Shachar Itzhaky; Noam Rinetzky (ESEC/SIGSOFT FSE, 2021)

Runtime Complexity Bounds Using Squeezers. - Oren Ish-Shalom; Shachar Itzhaky; Noam Rinetzky; Sharon Shoham (ACM Trans. Program. Lang. Syst., 2022)

State Merging with Quantifiers in Symbolic Execution. - David Trabish; Noam Rinetzky; Sharon Shoham; Vaibhav Sharma 001 (ESEC/SIGSOFT FSE, 2023)

Relaxed Effective Callback Freedom: A Parametric Correctness Condition for Sequential Modules With Callbacks. - Elvira Albert; Shelly Grossman; Noam Rinetzky; Clara Rodríguez-Núñez; Albert Rubio; Mooly Sagiv (IEEE Trans. Dependable Secur. Comput., 2023)