Paper Info
Title
FIXBAG: a fixpoint calculator for quantified bag constraints
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 sufficient for lower levels of program correctness. To analyze a wider range of programs, we have developed a tool to compute symbolic fixpoints for quantified 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.
Year
DOI
Venue
2011
10.1007/978-3-642-22110-1_53
CAV
Keywords
Field
DocType
stand-alone tool,better precision,program analysis,fixpoint analysis,recursive bag constraint,bag domain,acceptable precision,fixpoint calculator,program correctness,wider range,numerical domain
Calculator,Programming language,Abstract interpretation,Computer science,Correctness,Disjunctive normal form,Algorithm,Theoretical computer science,Loop invariant,Program analysis,Fixed point,Recursion
Conference
Citations 
PageRank 
References 
8
0.46
11
Authors
4
Name
Order
Citations
PageRank
Tuan Pham150373.75
Minh-Thai Trinh2723.49
Anh-Hoang Truong3264.98
Wei-Ngan Chin486863.37