Speeding Up logico-numerical strategy iteration

Monniaux, David and Schrammel, Peter (2014) Speeding Up logico-numerical strategy iteration. In: Static Analysis. Lecture Notes in Computer Science, 8723 . Springer, pp. 253-267. ISBN 9783319109350

[img] PDF - Accepted Version
Restricted to SRO admin only

Download (459kB)


We introduce an efficient combination of polyhedral analysis and predicate partitioning. Template polyhedral analysis abstracts numerical variables inside a program by one polyhedron per control location, with a priori fixed directions for the faces. The strongest inductive invariant in such an abstract domain may be computed by a combination of strategy iteration and SMT solving. Unfortunately, the above approaches lead to unacceptable space and time costs if applied to a program whose control states have been partitioned according to predicates. We therefore propose a modification of the strategy iteration algorithm where the strategies are stored succinctly, and the linear programs to be solved at each iteration step are simplified according to an equivalence relation. We have implemented the technique in a prototype tool and we demonstrate on a series of examples that the approach performs significantly better than previous strategy iteration techniques.

Item Type: Book Section
Keywords: static analysis, abstract interpretation, strategy iteration, logico-numerical systems, invariant inference
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User: Peter Schrammel
Date Deposited: 09 May 2016 10:37
Last Modified: 09 May 2016 10:37
URI: http://srodev.sussex.ac.uk/id/eprint/59926

View download statistics for this item

📧 Request an update