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 - Object Spreadsheets
- Live demo