Sciweavers

Share
CSL
2008
Springer

Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars

9 years 26 days ago
Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
Abstract. We present decision procedures for logical constraints involving collections such as sets, multisets, and fuzzy sets. Element membership in our collections is given by characteristic functions from a finite universe (of unknown size) to a user-defined subset of rational numbers. Our logic supports standard operators such as union, intersection, difference, or any operation defined pointwise using mixed linear integerrational arithmetic. Moreover, it supports the notion of cardinality of the collection, defined as the sum of occurrences of all elements. Deciding formulas in such logic has applications in software verification. Our decision procedure reduces satisfiability of formulas with collections to satisfiability of formulas in an extension of mixed linear integerrational arithmetic with a "star" operator. The star operator computes the integer cone (closure under vector addition) of the solution set of a given formula. We give an algorithm for eliminating the s...
Ruzica Piskac, Viktor Kuncak
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where CSL
Authors Ruzica Piskac, Viktor Kuncak
Comments (0)
books