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

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