LPAR
2010
Springer
13 years 8 months ago
2010
Springer
We describe a technique and a tool called Qex for generating input tables and parameter values for a given parameterized SQL query. The evaluation semantics of an SQL query is tra...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Abstract. We present a novel way for reasoning about (possibly ir)rational quantifier-free non-linear arithmetic by a reduction to SAT/SMT. The approach is incomplete and dedicated...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Data trees and data words have been studied extensively in connection with XML reasoning. These are trees or words that, in addition to labels from a finite alphabet, carry labels ...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
We introduce parameterized rewrite systems for describing infinite families of finite string rewrite systems depending upon non-negative integer parameters, as well as ways to reas...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Craig interpolation has become a key ingredient in many symbolic model checkers, serving as an approximative replacement for expensive quantifier elimination. In this paper, we foc...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Abstract. Recently, graded modalities have been added to the semantics of two of the logics most commonly used by the computer science community:
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Traditionally, the full verification of a program's functional correctness has been obtained with pen and paper or with interactive proof assistants, whereas only reduced ver...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Abstract. We introduce pairwise cardinality networks, networks of comparators, derived from pairwise sorting networks, which express cardinality constraints. We show that pairwise ...
LPAR
2010
Springer
13 years 8 months ago
2010
Springer
Abstract. We present ABC, a software tool for automatically computing symbolic upper bounds on the number of iterations of nested program loops. The system combines static analysis...