Polynomial template generation using sum-of-squares programming

File Description SizeFormat 
1409.3941v2.pdfWorking paper1.01 MBAdobe PDFView/Open
Title: Polynomial template generation using sum-of-squares programming
Authors: Adjé, A
Magron, V
Item Type: Report
Abstract: Template abstract domains allow to express more interesting properties than classical abstract domains. However, template generation is a challenging problem when one uses template abstract domains for program analysis. In this paper, we relate template generation with the program properties that we want to prove. We focus on one-loop programs with nested conditional branches. We formally define the notion of well-representative template basis with respect to such programs and a given property. The definition relies on the fact that template abstract domains produce inductive invariants. We show that these invariants can be obtained by solving certain systems of functional inequalities. Then, such systems can be strengthened using a hierarchy of sum-of-squares (SOS) problems when we consider programs written in polynomial arithmetic. Each step of the SOS hierarchy can possibly provide a solution which in turn yields an invariant together with a certificate that the desired property holds. The interest of this approach is illustrated on nontrivial program examples in polynomial arithmetic.
Issue Date: 18-Aug-2015
URI: http://hdl.handle.net/10044/1/25723
Copyright Statement: © 2014 The Authors
Notes: 23 pages, 3 figures, 1 table
Appears in Collections:Faculty of Engineering
Electrical and Electronic Engineering

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commonsx