×

zbMATH — the first resource for mathematics

Quicr: a reusable library for parametric abstraction of sets and numbers. (English) Zbl 1296.68004
Biere, Armin (ed.) et al., Computer aided verification. 26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08866-2/pbk). Lecture Notes in Computer Science 8559, 866-873 (2014).
Summary: This paper introduces QUICr, an abstract domain combinator library that lifts any domain for numbers into an efficient domain for numbers and sets of numbers. As a library, it is useful for inferring relational data invariants in programs that manipulate data structures. As a testbed, it allows easy extension of widening and join heuristics, enabling adaptations to new and varied applications. In this paper we present the architecture of the library, guidelines on how to select heuristics, and an example instantiation of the library using the Apron library to verify set-manipulating programs.
For the entire collection see [Zbl 1293.68018].

MSC:
68-04 Software, source code, etc. for problems pertaining to computer science
68N99 Theory of software
68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
Apron; FixBag; Quicr; SLAyer
PDF BibTeX XML Cite
Full Text: DOI