Polynomial Class of Constraints on Sets for Efficient Program Analysis
Speaker: Bruno Marnette , ENS de Cachan, MIT
Date: August 1 2005
Time: 4:00PM to 5:30PM
Location: G725
Host: Martin Rinard, CSAIL
Contact: Mary McDavitt, 617-253-9620, mmcdavit@csail.mit.edu
Relevant URL: 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.
We present complete polynomial-time algorithms for satisfiability and
entailment problems . The algorithms a based on a terminating rewriting
system which transforms i-trees into equivalent i-trees for which we can
easily decide satisfiability. We then give algorithm to extract complete
information from i-trees in normal form,allowing us to decide subsumption of i-trees.
See other events that are part of
See other events happening in August 2005
