Sciweavers

Share
LPAR
2010
Springer
9 years 6 months ago
Interpolating Quantifier-Free Presburger Arithmetic
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...
Daniel Kroening, Jérôme Leroux, Phili...
LPAR
2010
Springer
9 years 6 months ago
Graded Alternating-Time Temporal Logic
Abstract. Recently, graded modalities have been added to the semantics of two of the logics most commonly used by the computer science community:
Marco Faella, Margherita Napoli, Mimmo Parente
LPAR
2010
Springer
9 years 6 months ago
Dafny: An Automatic Program Verifier for Functional Correctness
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...
K. Rustan M. Leino
LPAR
2010
Springer
9 years 6 months ago
Pairwise Cardinality Networks
Abstract. We introduce pairwise cardinality networks, networks of comparators, derived from pairwise sorting networks, which express cardinality constraints. We show that pairwise ...
Michael Codish, Moshe Zazon-Ivry
LPAR
2010
Springer
9 years 6 months ago
ABC: Algebraic Bound Computation for Loops
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...
Régis Blanc, Thomas A. Henzinger, Thibaud H...
LPAR
2010
Springer
9 years 6 months ago
A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
Abstract. Jer
Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, ...
LPAR
2010
Springer
9 years 6 months ago
Coping with Selfish On-Going Behaviors
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 ...
Orna Kupferman, Tami Tamir
LPAR
2010
Springer
9 years 6 months ago
On the Equality of Probabilistic Terms
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...
Gilles Barthe, Marion Daubignard, Bruce M. Kapron,...
books