FixBag: A Fixpoint Calculator for Quantified Bag Constraints

Autor:	Anh-Hoang Truong, Minh-Thai Trinh, Tuan-Hung Pham, Wei-Ngan Chin
Rok vydání:	2011
Předmět:	Range (mathematics) Loop invariant Program analysis Theoretical computer science Correctness Calculator Computer science law Disjunctive normal form Abstract interpretation Algorithm law.invention Domain (software engineering)
Zdroj:	Computer Aided Verification ISBN: 9783642221095 CAV
DOI:	10.1007/978-3-642-22110-1_53
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::31023d1b1c141643a84553c75b226312 https://doi.org/10.1007/978-3-642-22110-1_53 Zobrazit plný text záznamu