A simple inductive synthesis methodology and its applications. - Shachar Itzhaky; Sumit Gulwani; Neil Immerman; Mooly Sagiv (OOPSLA, 2010)

Effectively-Propositional Reasoning about Reachability in Linked Data Structures. - Shachar Itzhaky; Anindya Banerjee 001; Neil Immerman; Aleksandar Nanevski; Mooly Sagiv (CAV, 2013)

Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning. - Shachar Itzhaky; Sumit Gulwani; Neil Immerman; Mooly Sagiv (LPAR, 2013)

Property-Directed Shape Analysis. - Shachar Itzhaky; Nikolaj S. Bjørner; Thomas W. Reps; Mooly Sagiv; Aditya V. Thakur (CAV, 2014)

VeriCon: towards verifying controller programs in software-defined networks. - Thomas Ball 001; Nikolaj S. Bjørner; Aaron Gember; Shachar Itzhaky; Aleksandr Karbyshev; Mooly Sagiv; Michael Schapira; Asaf Valadarsky (PLDI, 2014)

Modular reasoning about heap paths via effectively propositional formulas. - Shachar Itzhaky; Anindya Banerjee 001; Neil Immerman; Ori Lahav 001; Aleksandar Nanevski; Mooly Sagiv (POPL, 2014)

Automatic reasoning for pointer programs using decidable logics / Itzhaky Shachar - Shachar Itzhaky (2014)

Deriving divide-and-conquer dynamic programming algorithms using solver-aided transformations. - Shachar Itzhaky; Rohit Singh 002; Armando Solar-Lezama; Kuat Yessenov; Yongquan Lu; Charles E. Leiserson; Rezaul Alam Chowdhury (OOPSLA, 2016)

Object spreadsheets: a new computational model for end-user development of data-centric web applications. - Matt McCutchen; Shachar Itzhaky; Daniel Jackson 001 (Onward!, 2016)

Verified lifting of stencil computations. - Shoaib Kamil 001; Alvin Cheung; Shachar Itzhaky; Armando Solar-Lezama (PLDI, 2016)

Type-Driven Repair for Information Flow Security. - Nadia Polikarpova; Jean Yang 001; Shachar Itzhaky; Armando Solar-Lezama (CoRR, 2016)

Verifying Equivalence of Spark Programs. - Shelly Grossman; Sara Cohen; Shachar Itzhaky; Noam Rinetzky; Mooly Sagiv (CAV (2), 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)

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)

Abstraction-Based Interaction Model for Synthesis. - Hila Peleg; Shachar Itzhaky; Sharon Shoham (VMCAI, 2018)

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)

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)

Programming by predicates: a formal model for interactive synthesis. - Hila Peleg; Shachar Itzhaky; Sharon Shoham; Eran Yahav (Acta Informatica, 2020)

Programming with a read-eval-synth loop. - Hila Peleg; Roi Gabay; Shachar Itzhaky; Eran Yahav (Proc. ACM Program. Lang., 2020)

Liquid information flow control. - Nadia Polikarpova; Deian Stefan; Jean Yang 001; Shachar Itzhaky; Travis Hance; Armando Solar-Lezama (Proc. ACM Program. Lang., 2020)

Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper). - Shachar Itzhaky; Hila Peleg; Nadia Polikarpova; Reuben N. S. Rowe; Ilya Sergey (CAV (1), 2021)

Theory Exploration Powered by Deductive Synthesis. - Eytan Singher; Shachar Itzhaky (CAV (2), 2021)

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)

Cyclic program synthesis. - Shachar Itzhaky; Hila Peleg; Nadia Polikarpova; Reuben N. S. Rowe; Ilya Sergey (PLDI, 2021)

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

AmiGo: Computational Design of Amigurumi Crochet Patterns. - Michal Edelstein; Hila Peleg; Shachar Itzhaky; Mirela Ben-Chen (SCF, 2022)

Securing Access to Untrusted Services From TEEs with GateKeeper. - Meni Orenbach; Bar Raveh; Alon Berkenstadt; Yan Michalevsky; Shachar Itzhaky; Mark Silberstein (CoRR, 2022)

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

SMT Sampling via Model-Guided Approximation. - Matan Peled; Bat-Chen Rothenberg; Shachar Itzhaky (FM, 2023)

Scalable Spreadsheet-Driven End-User Applications with Incremental Computation. - Sean Hadar; Shachar Itzhaky (Onward!, 2023)

Colored E-Graph: Equality Reasoning with Conditions. - Eytan Singher; Shachar Itzhaky (CoRR, 2023)

Leveraging Rust Types for Program Synthesis. - Jonás Fiala; Shachar Itzhaky; Peter Müller 001; Nadia Polikarpova; Ilya Sergey (Proc. ACM Program. Lang., 2023)

Constrictor: Immutability as a Design Concept. - Elad Kinsbruner; Shachar Itzhaky; Hila Peleg (ECOOP, 2024)

Hyperproperty Verification as CHC Satisfiability. - Shachar Itzhaky; Sharon Shoham; Yakir Vizel (ESOP (2), 2024)

Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions. - Eytan Singher; Shachar Itzhaky (FMCAD, 2024)

Kotlin's Type System is (Also) Unsound. - Elad Kinsbruner; Hila Peleg; Shachar Itzhaky (CoRR, 2024)

Constrictor: Immutability as a Design Concept (Artifact). - Elad Kinsbruner; Shachar Itzhaky; Hila Peleg (Dagstuhl Artifacts Ser., 2024)

CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs. - Cole Kurashige; Ruyi Ji; Aditya Giridharan; Mark Barbone; Daniel Noor; Shachar Itzhaky; Ranjit Jhala; Nadia Polikarpova (Proc. ACM Program. Lang., 2024)

Dynamic Robustness Verification against Weak Memory. - Roy David Margalit; Michalis Kokologiannakis; Shachar Itzhaky; Ori Lahav 001 (Proc. ACM Program. Lang., 2025)

Dynamic Robustness Verification Against Weak Memory (Extended Version). - Roy David Margalit; Michalis Kokologiannakis; Shachar Itzhaky; Ori Lahav 001 (CoRR, 2025)