# The ICICS/CS Reading Room

## UBC CS TR-2005-19 Summary

- A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs, September 19, 2005 Jesse Bingham and Zvonimir Rakamaric, 28 pages
An important and ubiquitous class of programs are heap-manipulating programs
(HMP), which manipulate unbounded linked data structures by following pointers
and updating links. Predicate abstraction has proved to be an invaluable
technique in the field of software model checking; this technique relies on an
efficient decision procedure for the underlying logic. The expression
and
proof of many interesting HMP safety properties require transitive closure
predicates; such predicates express that some node can be reached from another
node by following a sequence of (zero or more) links in the data structure.
Unfortunately, adding support for transitive closure often yields
undecidability, so one must be careful in defining such a logic. Our primary
contributions are the definition of a simple transitive closure logic for use
in predicate abstraction of HMPs, and a decision procedure for this logic.
Through several experimental examples, we demonstrate that our logic is
expressive enough to prove interesting properties with predicate abstraction,
and that our decision procedure provides us with both a time and space
advantage over previous approaches.

If you have any questions or comments regarding this page please send mail to
help@cs.ubc.ca.