Shachar Itzhaky
A Minimalist Web Page

Well, Hi.

Publications

Effectively-Propositional Reasoning About Reachability in Linked Data Structures Abstract  PDF
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv 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 the Proceedings of the ACM SPLASH Conference (SPLASH 2010), Reno, NV, United States, October 2010.

Pending

VeriCon: Towards Verifying Controller Programs in Software-Defined Networks
(as co-author, pending submission to PLDI)

Property-Guided Shape Analysis
(pending submission to TACAS)

Modular Reasoning about Heap Paths via Effectively Propositional Formulas
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv To appear in 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
Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv To appear in LPAR-19, Stellenbosch, South Africa, December 2013

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
Source code (incl. dependencies, about 6M)
Figure (2D Graphics Synthesis)
Windows: Figure-win32-101202.zip (32M)
Mac: Figure-udzo-101202.dmg (24M)

Users are encouraged to download the STIX fonts package (free) for enhanced display of mathmatical symbols in formulas.