Shachar Itzhaky
A Minimalist Web Page me

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 kl 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  PDFObject 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 ComputationsAbstract  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 AbsenceAbstract  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 AnalysisAbstract  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 NetworksAbstract  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 FormulasAbstract  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 ReasoningAbstract  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 StructuresAbstract  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 ApplicationsAbstract  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 SecurityPDF
Nadia Polikarpova, Jean Yang, Shachar Itzhaky, Armando Solar-Lezama

Effectively-Propositional Reasoning About Reachability in Linked Data StructuresPDF
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv

Solving Geometry Problems Using a Combination of Symbolic and Numerical ReasoningAbstract  PDF
Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv

Thesis

Automatic Reasoning for Pointer Programs Using Decidable LogicsPDF
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