Overview
Bohne is a symbolic shape analysis tool. It infers loop invariants of programs manipulating heap-allocated data structures. Bohne is integrated into the Jahob verification system. A standalone version of Bohne will be available, soon.
Related Publications
- Heap Assumptions on Demand with Andreas Podelski and Andrey Rybalchenko
In Proceedings of CAV, 2008. [pdf] [pdf-extended] - Verifying Complex Properties using Symbolic Shape Analysis with Viktor Kuncak, Karen Zee, Andreas Podelski, and Martin Rinard
Workshop on Heap Abstraction and Verification, March 2007. [pdf] - Field Constraint Analysis with Viktor Kuncak, Patrick Lam, Andreas Podelski, and Martin Rinard
In Proceedings of VMCAI, 2006. [pdf] [pdf-extended] [pdf-slides] - Boolean Heaps with Andreas Podelski
In Proceedings of SAS, 2005. [pdf] [pdf-slides]