FixBag: A Fixpoint Calculator for Quantified Bag Constraints
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal Title
Journal ISSN
Volume Title
Title
FixBag: A Fixpoint Calculator for Quantified Bag Constraints
Published Date
2011
Publisher
Type
Report
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.
Keywords
Description
Associated research group: Critical Systems Research Group
Related to
Replaces
License
Series/Report Number
Funding information
Isbn identifier
Doi identifier
Previously Published Citation
23rd International Conference onComputer Aided Verification (CAV'11)
Suggested citation
Pham, Hung T.; Trinh, Minh-Thai; Truong, Anh-Hoang; Chin, Wei-Ngan. (2011). FixBag: A Fixpoint Calculator for Quantified Bag Constraints. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217398.
Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.