Well, Hi.

I am a senior lecturer at Technion, Haifa. My research areas include functional languages, synthesis of functional programs, and high-level programming. This is my current research statement.

# Publications

**Hyperproperty Verification as CHC Satisfiability** Abstract

Shachar Itzhaky, Sharon Shoham, Yakir Vizel. *In ESOP 2024 (European Symposium on Programming, April 2024) *

Hyperproperties govern the behavior of a system or systems across multiple executions, and are being recognized as an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by modern software model-checking approaches such as IC3/PDR, due to the need to find not only an inductive invariant but also a *total* alignment of different executions that facilitates simpler inductive invariants. We show how this treatment is achieved via a reduction from the verification problem of ∀^{k}∃^{l} properties to Constrained Horn Clauses. The approach is based on combining the inference of an alignment and inductive invariant in a single CHC encoding; and, for existential quantification over traces, incorporating also inference of a witness function for the existential choices, based on a game semantics with a sound-and-complete encoding to CHCs as well.

**Leveraging Rust Types for Program Synthesis**

Jonás Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, Ilya Sergey. *In Proc. ACM Program. Lang. 2023 *

**SMT Sampling via Model-Guided Approximation**

Matan Peled, Bat-Chen Rothenberg, Shachar Itzhaky. *In Formal Methods - 25th International Symposium, FM 2023 *

**Scalable Spreadsheet-Driven End-User Applications with Incremental Computation**

Sean Hadar, Shachar Itzhaky. *In Proceedings of the 2023 *

**AmiGo: Computational Design of Amigurumi Crochet Patterns**

Michal Edelstein, Hila Peleg, Shachar Itzhaky, Mirela Ben-Chen. *In SCF '22: Proceedings of the 7th Annual ACM Symposium on Computational Fabrication, Seattle, WA, USA, October 26-28, 2022 *

**Run-Time Complexity Bounds Using Squeezers** Abstract

Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham. *In ESOP 2021 (European Symposium on Programming, March 2021) *

**Programming by Predicates: a Formal Model for Interactive Synthesis**

Hila Peleg, Shachar Itzhaky, Sharon Shoham, Eran Yahav. *In Acta Informatica 2020 *

**Liquid Information Flow Control** Abstract

Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama. *In ICFP 2020 (ACM SIGPLAN International Conference on Functional Programming, August 2020) *

**Programming with a Read-Eval-Synth Loop**

Hila Peleg, Roi Gabay, Shachar Itzhaky, Eran Yahav. *In OOPSLA 2020 (ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity (OOPSLA track), 2020) *

**Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction**

Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham. *In VMCAI 2020 (International Conference on Verification, Model Checking, and Abstract Interpretation, January 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. *In VMCAI 2020 (International Conference on Verification, Model Checking, and Abstract Interpretation, January 2020) *

**Property-Directed Inference of Universal Invariants or Proving Their Absence** – extended version

Aleksander Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham. *In JACM 2017 (Journal of the ACM, 2017) *

**Deriving Divide-and-Conquer Dynamic Programming Algorithms Using Solver-Aided Transformations** Abstract

Shachar Itzhaky, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov, Yongquan Lu, Charles Leiserson, Rezaul Chowdhury. *In OOPSLA 2016 (ACM SIGPLAN conference on Systems, Programming, Languages, and Applications: Software for Humanity (OOPSLA track), Amsterdam, Netherlands, November 2016) *

Abstract PDF**Object Spreadsheets: a New Computational Model for End-user Development of Data-centric Web Applications**

Richard Matthew McCutchen, Shachar Itzhaky, Daniel Jackson *In SPLASH 2016 Onward! (to appear November 2016)*

**Verified Lifting of Stencil Computations**Abstract PDF

Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, and Armando Solar-Lezama *In PLDI 2016 (37th ACM SIGPLAN Conference on Programming Language Design and Implementation, Santa Barbara, CA, USA, June 2016)*

**Property-Directed Inference of Universal Invariants or Proving Their Absence**Abstract PDF

Aleksander Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham *In CAV 2015 (Computer Aided Verification, San Francisco, CA, USA, July 2015)*

**Property-Directed Shape Analysis**Abstract PDF

Shachar Itzhaky, Nikolaj Bjørner, Thomas Reps, Mooly Sagiv, Aditya Thakur *In CAV 2014 (Computer Aided Verification, Vienna, Austria, July 2014)*

**VeriCon: Towards Verifying Controller Programs in Software-Defined Networks**Abstract PDF

Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, Asaf Valadarsky *In PLDI 2014 (35th ACM SIGPLAN Conference on Programming Language Design and Implementation, Edinburgh, UK, June 2014)*

**Modular Reasoning about Heap Paths via Effectively Propositional Formulas**Abstract PDF

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv *In POPL 2014 (41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 2014)*

**Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning**Abstract PDF

Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv *In LPAR-19, Stellenbosch, South Africa, December 2013*

**Effectively-Propositional Reasoning About Reachability in Linked Data Structures**Abstract PDF

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv *In CAV 2013 (Computer Aided Verification, 2013, St. Petersburg, Russia, July 2013)*

**A Simple Inductive Synthesis Methodology and Its Applications**Abstract BibTeX PDF

Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv *In SPLASH 2010 (ACM SIGPLAN Conference on Systems, Programming, Languages and Applications: Software for Humanity, Reno, NV, United States, October 2010)*

# Technical Reports and Archives

**Type-Driven Repair for Information Flow Security****PDF**

Nadia Polikarpova, Jean Yang, Shachar Itzhaky, Armando Solar-Lezama

**Effectively-Propositional Reasoning About Reachability in Linked Data Structures****PDF**

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv

**Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning****Abstract PDF**

Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv

# Thesis

**Automatic Reasoning for Pointer Programs Using Decidable Logics**PDF

Under the supervision of Professor Mooly Sagiv *Tel Aviv University (submitted: August 2014; approved: July 2015)**Recipient of the ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award*

# My Codez

- EPR-based Verification
- PDR
^{∀}– loop invariant inference

MacUbuntu 64-bit, 32-bit - VeriCon – Hoare-style verification for SDN controller programs
- Source
- Object Spreadsheets
- Live demo