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.*

This paper proposes a novel method of harnessing existing SAT solvers to verify
reachability properties of programs that manipulate linked-list data structures. Such properties
are essential for proving program termination, correctness of data structure
invariants, and other safety properties. Our solution is complete,
i.e., a SAT solver produces a counterexample whenever a program
does not satisfy its specification. This result is
surprising since even first-order theorem provers usually cannot deal
with reachability in a complete way, because doing so requires reasoning about
transitive closure.

Our result is based on the following ideas:

- Programmers must write assertions in a restricted logic without quantifier alternation or function symbols.
- The correctness of many programs can be expressed in such restricted logics, although we explain the tradeoffs.
- Recent results in descriptive complexity can be utilized to show that every program that manipulates
potentially cyclic, singly- and doubly-linked lists and that is annotated with assertions written in this restricted logic, can be verified with a SAT solver.

We implemented a tool atop Z3 and used it to show the correctness of several linked list programs.

**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.*

Given a high-level specification and a low-level programming language, our goal is to automatically
synthesize an efficient program that meets the specification. In this paper, we present a new
algorithmic methodology for inductive synthesis that allows us to do this.

We use Second Order logic as our generic high level specification logic. For our low-level
languages we choose small application-specific logics that can be immediately translated into code
that runs in expected linear time in the worst case.

We explain our methodology and provide examples of the synthesis of several graph classifiers, e.g,
linear-time tests of whether the input graph is connected, acyclic, etc. In another set of
applications we automatically derive many finite differencing expressions equivalent to ones that
Paige built by hand in his thesis. Finally we describe directions for
automatically combining such automatically generated building blocks to synthesize efficient code
implementing more complicated specifications.

The methods in this paper have been implemented in Python using the SMT solver Z3.

## 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

We describe a framework that combines deductive, numeric, and inductive
reasoning to solve geometric problems. Applications include the generation of
geometric models and animations, as well as problem solving in the context of
intelligent tutoring systems.

Our novel methodology uses (i) deductive reasoning to generate a partial program from logical
constraints, (ii) numerical methods to evaluate the partial program, thus creating geometric models
which are solutions to the original problem, and (iii) inductive synthesis to read off new
constraints that are then applied to one more round of deductive reasoning leading to the desired
deterministic program. By the combination of methods we were able to solve
problems that each of the methods was not able to solve by itself.

The number of nondeterministic choices in a partial program provides a
measure of how close a problem is to being solved and can thus be used in the educational context for grading and providing hints.

We have successfully evaluated our methodology on 18
Scholastic Aptitude Test geometry problems, and 11 ruler/compass-based
geometry construction problems. Our tool solved these problems using an
average of a few seconds per problem.

# 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.