Symbolic Polytopes for Quantitative Verification

Klaus von Gleissenthall

14th May 2015 (Thursday), 10:00 in KE322

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.
This talk presents a novel algorithm for synthesizing formulas for given cardinality constraints, which relies on the theory of counting integral points in symbolic polytopes. The algorithm is cast in terms of a cardinality-constrained interpolation procedure, which is put to work in a solver for recursive Horn clauses with cardinality constraints based on abstraction refinement. I will conclude with an experimental evaluation on a number of representative examples.

The talk is based on joint work with Boris Köpf and Andrey Rybalchenko.

Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc  seadmissions@le.ac.uk
E: MSc  pgadmissions@le.ac.uk

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604
E: csadmin@mcs.le.ac.uk

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom

Accessibility

DisabledGo logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.