FixBag: A Fixpoint Calculator for Quantified Bag Constraints. 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.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Li, Huisong; Berenger, Francois; Chang, Bor-Yuh Evan; Rival, Xavier: Semantic-directed clumping of disjunctive abstract states (2017)
- Cox, Arlen; Chang, Bor-Yuh Evan; Sankaranarayanan, Sriram: Quicr: a reusable library for parametric abstraction of sets and numbers (2014)
- Qin, Shengchao; He, Guanhua; Chin, Wei-Ngan; Yang, Hongli: Invariants synthesis over a combined domain for automated program verification (2013)
- Pham, Tuan-Hung; Trinh, Minh-Thai; Truong, Anh-Hoang; Chin, Wei-Ngan: Fixbag: A fixpoint calculator for quantified bag constraints (2011) ioport