2014/11/21 by Adjé, Assalé, Garoche, Pierre-Loïc, Werey, Alexis
#D.2.4 #F.3.1 #F.3.2 #FOS: Computer and information sciences #FOS: Mathematics #G.1.0 #G.1.6 #Logic in Computer Science (cs.LO) #Optimization and Control (math.OC)
paper · doi:10.48550/arxiv.1411.5847
Affine forms are a common way to represent convex sets of ℝ using a base of error terms ε∈ [-1, 1]m. Quadratic forms are an extension of affine forms enabling the use of quadratic error terms εi εj. In static analysis, the zonotope domain, a relational abstract domain based on affine forms has been used in a wide set of settings, e.g. set-based simulation for hybrid systems, or floating point analysis, providing relational abstraction of functions with a cost linear in the number of errors terms. In this paper, we propose a quadratic version of zonotopes. We also present a new algorithm based on semi-definite programming to project a quadratic zonotope, and therefore quadratic forms, to intervals. All presented material has been implemented and applied on representative examples.