| 2021 | ESOP | Run-time Complexity Bounds Using Squeezers. | Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2021 | ICST | Address-Aware Query Caching for Symbolic Execution. | David Trabish, Shachar Itzhaky, Noam Rinetzky |
| 2020 | ISSTA | Relocatable addressing model for symbolic execution. | David Trabish, Noam Rinetzky |
| 2020 | VMCAI | 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 |
| 2020 | VMCAI | Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction. | Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2019 | ICDE | COBRA: Compression Via Abstraction of Provenance for Hypothetical Reasoning. | Daniel Deutch, Yuval Moskovitch, Noam Rinetzky |
| 2019 | PLDI | 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 |
| 2019 | PLDI | Computing summaries of string loops in C for better testing and refactoring. | Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Cristian Cadar |
| 2019 | SIGMOD | Hypothetical Reasoning via Provenance Abstraction. | Daniel Deutch, Yuval Moskovitch, Noam Rinetzky |
| 2018 | ASPLOS | Statistical Reconstruction of Class Hierarchies in Binaries. | Omer Katz, Noam Rinetzky, Eran Yahav |
| 2018 | EDBT | Towards Hypothetical Reasoning Using Distributed Provenance. | Daniel Deutch, Yuval Moskovitch, Itay Polak, Noam Rinetzky |
| 2018 | ICSE | Chopped symbolic execution. | David Trabish, Andrea Mattavelli, Noam Rinetzky, Cristian Cadar |
| 2018 | PPoPP | Safe privatization in transactional memory. | Artem Khyzha, Hagit Attiya, Alexey Gotsman, Noam Rinetzky |
| 2017 | CAV | Verifying Equivalence of Spark Programs. | Shelly Grossman, Sara Cohen, Shachar Itzhaky, Noam Rinetzky, Mooly Sagiv |
| 2017 | ICDT | On the Automated Verification of Web Applications with Embedded SQL. | Shachar Itzhaky, Tomer Kotek, Noam Rinetzky, Mooly Sagiv, Orr Tamir, Helmut Veith, Florian Zuleger |
| 2017 | SAS | Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs. | Suvam Mukherjee, Oded Padon, Sharon Shoham, Deepak D'Souza, Noam Rinetzky |
| 2017 | VMCAI | Conjunctive Abstract Interpretation Using Paramodulation. | Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv |
| 2016 | CAV | From Shape Analysis to Termination Analysis in Linear Time. | Roman Manevich, Boris Dogadov, Noam Rinetzky |
| 2016 | VMCAI | Property Directed Abstract Interpretation. | Noam Rinetzky, Sharon Shoham |
| 2015 | CAV | Property-Directed Inference of Universal Invariants or Proving Their Absence. | Aleksandr Karbyshev, Nikolaj S. Bjrner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2015 | FMCAD | Pattern-based Synthesis of Synchronization for the C++ Memory Model. | Yuri Meshman, Noam Rinetzky, Eran Yahav |
| 2015 | OPODIS | A Heap-Based Concurrent Priority Queue with Mutable Priorities for Faster Parallel Algorithms. | Orr Tamir, Adam Morrison, Noam Rinetzky |
| 2015 | SAS | 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 |
| 2014 | PODC | Brief announcement: concurrency-aware linearizability. | Nir Hemed, Noam Rinetzky |
| 2013 | ESOP | Verifying Concurrent Memory Reclamation Algorithms with Grace. | Alexey Gotsman, Noam Rinetzky, Hongseok Yang |
| 2013 | PODC | A programming language perspective on transactional memory consistency. | Hagit Attiya, Alexey Gotsman, Sandeep Hans, Noam Rinetzky |
| 2010 | PODC | Verifying linearizability with hindsight. | Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, Greta Yorsh |
| 2010 | POPL | Sequential verification of serializability. | Hagit Attiya, G. Ramalingam, Noam Rinetzky |
| 2009 | ESOP | Abstraction for Concurrent Objects. | Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang |
| 2008 | ISSTA | Verifying dereference safety via expanding-scope analysis. | Alexey Loginov, Eran Yahav, Satish Chandra, Stephen Fink, Noam Rinetzky, Mangala Gowri Nanda |
| 2007 | APLAS | Local Reasoning for Storable Locks and Threads. | Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, Mooly Sagiv |
| 2007 | CAV | Comparison Under Abstraction for Verifying Linearizability. | Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav |
| 2007 | ESOP | Modular Shape Analysis for Dynamically Encapsulated Programs. | Noam Rinetzky, Arnd Poetzsch-Heffter, Ganesan Ramalingam, Mooly Sagiv, Eran Yahav |
| 2007 | PLDI | CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors. | Martin T. Vechev, Eran Yahav, David F. Bacon, Noam Rinetzky |
| 2005 | POPL | A semantics for procedure local heaps and its abstractions. | Noam Rinetzky, Jrg Bauer, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2005 | SAS | Interprocedural Shape Analysis for Cutpoint-Free Programs. | Noam Rinetzky, Mooly Sagiv, Eran Yahav |
| 2001 | CC | Interprocedural Shape Analysis for Recursive Programs. | Noam Rinetzky, Shmuel Sagiv |