LPAR
2010
Springer
13 years 2 months ago
2010
Springer
LPAR
2010
Springer
13 years 2 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 2 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 2 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 2 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 2 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...
LPAR
2010
Springer
13 years 2 months ago
2010
Springer
Abstract. Jer
LPAR
2010
Springer
13 years 2 months ago
2010
Springer
LPAR
2010
Springer
13 years 2 months ago
2010
Springer
A rational and selfish environment may have an incentive to cheat the system it interacts with. Cheating the system amounts to reporting a stream of inputs that is different from ...
LPAR
2010
Springer
13 years 2 months ago
2010
Springer
We consider a mild extension of universal algebra in which terms are built both from deterministic and probabilistic variables, and are interpreted as distributions. We formulate a...