IIV: An Invisible Invariant Verifier. - Ittai Balaban; Yi Fang 001; Amir Pnueli; Lenore D. Zuck (CAV, 2005)

Ranking Abstraction as Companion to Predicate Abstraction. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (FORTE, 2005)

Refactoring support for class library migration. - Ittai Balaban; Frank Tip; Robert M. Fuhrer (OOPSLA, 2005)

Shape Analysis by Predicate Abstraction. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (VMCAI, 2005)

Invisible Safety of Distributed Protocols. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (ICALP (2), 2006)

Ranking Abstraction of Recursive Programs. - Ittai Balaban; Ariel Cohen 002; Amir Pnueli (VMCAI, 2006)

Shape Analysis of Single-Parent Heaps. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (VMCAI, 2007)

Modular Ranking Abstraction. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (Int. J. Found. Comput. Sci., 2007)

Shape Analysis by Abstraction, Augmentation, and Transformation. - Ittai Balaban (2007)

Proving the Refuted: Symbolic Model Checkers as Proof Generators. - Ittai Balaban; Amir Pnueli; Lenore D. Zuck (Concurrency, Compositionality, and Correctness, 2010)

Refactoring using type constraints. - Frank Tip; Robert M. Fuhrer; Adam Kiezun; Michael D. Ernst; Ittai Balaban; Bjorn De Sutter (ACM Trans. Program. Lang. Syst., 2011)

Verification of multi-linked heaps. - Ittai Balaban; Amir Pnueli; Yaniv Sa'ar; Lenore D. Zuck (J. Comput. Syst. Sci., 2012)