Xisa is an automatic program analysis and verification tool for reasoning about recursive data structures, such as pointer-based lists and trees. The Xisa approach is unique in that it utilizes high-level, program developer-oriented specifications to focus the analysis to properties of interest to the developer.

Shape analyses, like Xisa, are particularly important in that they can capture detailed aliasing and structural information that is typically beyond the ability of other static program analyses. To be precise and scalable, they need to use program-specific abstractions. Unlike other approaches that are typically either insufficiently customizable or require low-level, expert interaction, Xisa builds program-specific abstractions using high-level, inductive predicates analogous to data structure validation code (e.g., a pretty-printer of a data structure written by developers for testing or dynamic analysis). In the end, Xisa presents program invariants about the memory state in the form of graphical diagrams roughly comparable to those that would appear on a whiteboard or in a textbook.

For more details and examples, please see the demonstration page.

Papers

Talks

Related Projects