Polynomial Class of Constraints on Sets for Efficient Program Analysis
Speaker: Bruno Marnette , ENS de Cachan, MIT
Typestate systems ensure many desirable properties of imperative programs. Abstract sets with cardinality constraints naturally generalize typestate properties: relationships between the typestates of objects can be expressed as subset and disjointness relations on sets, and elements of sets can be represented as sets of cardinality one. In addition, sets with cardinality constraints provide a natural language for specifying operations and invariants of data structures. We present a new class of constraints for sets with cardinalities (i-trees) that can serve as a foundation for efficient program analysis.