Shachar Itzhaky
A Minimalist Web Page

Well, Hi.

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

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