University of Minnesota
Software Engineering Center
/

You are here

FixBag: A Fixpoint Calculator for Quantified Bag Constraints

Date of Publication: 
July 2011
Associated Research Groups: 
Publication Files: 
Abstract: 
Abstract interpretation techniques have played a major role in advancing the state-of-the-art in program analysis. Traditionally, stand- alone tools for these techniques have been developed for the numerical domains which may be sucient for lower levels of program correctness. To analyze a wider range of programs, we have developed a tool to compute symbolic xpoints for quantied bag domain. This domain is useful for programs that deal with collections of values. Our tool is able to derive both loop invariants and method pre/post conditions via fixpoint analysis of recursive bag constraints. To support better precision, we have allowed disjunctive formulae to be inferred, where appropriate. As a stand-alone tool, we have tested it on a range of small but challenging examples with acceptable precision and performance.
Venue: 
23rd International Conference onComputer Aided Verification (CAV'11)