Paper Info
Title
Symbolic Polytopes For Quantitative Interpolation And Verification
Abstract
Proving quantitative properties of programs, such as bounds on resource usage or information leakage, often leads to verification conditions that involve cardinalities of sets. Existing approaches for dealing with such verification conditions operate by checking cardinality bounds for given formulas. However, they cannot synthesize formulas that satisfy given cardinality constraints, which limits their applicability for inferring cardinality-based inductive arguments.In this paper we present an algorithm for synthesizing formulas for given cardinality constraints, which relies on the theory of counting integer points in symbolic polytopes. We cast our algorithm in terms of a cardinality-constrained interpolation procedure, which we put to work in a solver for recursive Horn clauses with cardinality constraints based on abstraction refinement. We implement our technique and describe its evaluation on a number of representative examples.
Year
DOI
Venue
2015
10.1007/978-3-319-21690-4_11
COMPUTER AIDED VERIFICATION, PT I
Field
DocType
Volume
Horn clause,Information leakage,Computer science,Interpolation,Cardinality,Theoretical computer science,Polytope,Linear arithmetic
Conference
9206
ISSN
Citations 
PageRank 
0302-9743
4
0.38
References 
Authors
26
3
Name
Order
Citations
PageRank
Klaus von Gleissenthall1213.47
Boris Köpf259925.51
Andrey Rybalchenko3143968.53