Shachar Itzhaky
A Minimalist Web Page

Well, Hi.

I am a postdoctoral associate at MIT CSAIL, in the Computer Aided Programming group headed by Prof. Armando Solar-Lezama. My research areas include functional languages, synthesis of functional programs, and high-level programming.

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)

Publications

Deriving Divide-and-Conquer Dynamic Programming Algorithms Using Solver-Aided Transformations Abstract  PDF
Shachar Itzhaky, Rohit Singh, Armando Solar-Lezama, Kuat Yessenov, Yongquan Lu, Charles Leiserson, Rezaul Chowdhury In SPLASH 2016 OOPSLA (to appear 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

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

Software

EPR-based Verification
PDR – loop invariant inference
Mac Ubuntu 64-bit, 32-bit
VeriCon – Hoare-style verification for SDN controller programs
Source
Object Spreadsheets
Live demo