| 2026 | CPP | Enhancing Symbolic Execution with Machine-Checked Safety Proofs. | David Trabish, Shachar Itzhaky |
| 2026 | IJCAR | Automatic Abstraction Refinement for Hyperproperties Verification. | Malak Marrid, Shachar Itzhaky, Sharon Shoham, Yakir Vizel |
| 2025 | SAS | Ductape: Optimizing Dynamically Typed Programs Using Ahead-of-Time Compilation and Data-Flow Analysis. | Adi Harif, Shachar Itzhaky |
| 2024 | ECOOP | Constrictor: Immutability as a Design Concept. | Elad Kinsbruner, Shachar Itzhaky, Hila Peleg |
| 2024 | ESOP | Hyperproperty Verification as CHC Satisfiability. | Shachar Itzhaky, Sharon Shoham, Yakir Vizel |
| 2024 | FMCAD | Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions. | Eytan Singher, Shachar Itzhaky |
| 2023 | FM | SMT Sampling via Model-Guided Approximation. | Matan Peled, Bat-Chen Rothenberg, Shachar Itzhaky |
| 2023 | Onward | Scalable Spreadsheet-Driven End-User Applications with Incremental Computation. | Sean Hadar, Shachar Itzhaky |
| 2021 | CAV | Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper). | Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey |
| 2021 | CAV | Theory Exploration Powered by Deductive Synthesis. | Eytan Singher, Shachar Itzhaky |
| 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 |
| 2021 | PLDI | Cyclic program synthesis. | Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey |
| 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 | PLDI | Computing summaries of string loops in C for better testing and refactoring. | Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Cristian Cadar |
| 2018 | VMCAI | Abstraction-Based Interaction Model for Synthesis. | Hila Peleg, Shachar Itzhaky, Sharon Shoham |
| 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 |
| 2016 | OOPSLA | Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations. | Shachar Itzhaky, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov, Yongquan Lu, Charles E. Leiserson, Rezaul Alam Chowdhury |
| 2016 | OOPSLA | Object spreadsheets: a new computational model for end-user development of data-centric web applications. | Matt McCutchen, Shachar Itzhaky, Daniel Jackson |
| 2016 | PLDI | Verified lifting of stencil computations. | Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, Armando Solar-Lezama |
| 2015 | CAV | Property-Directed Inference of Universal Invariants or Proving Their Absence. | Aleksandr Karbyshev, Nikolaj S. Bjrner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham |
| 2014 | CAV | Property-Directed Shape Analysis. | Shachar Itzhaky, Nikolaj S. Bjrner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur |
| 2014 | PLDI | VeriCon: towards verifying controller programs in software-defined networks. | Thomas Ball, Nikolaj S. Bjrner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky |
| 2014 | POPL | Modular reasoning about heap paths via effectively propositional formulas. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv |
| 2013 | CAV | Effectively-Propositional Reasoning about Reachability in Linked Data Structures. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv |
| 2013 | LPAR | Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning. | Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv |
| 2010 | OOPSLA | A simple inductive synthesis methodology and its applications. | Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv |