Schrammel, Peter and Subotic, Pavle (2013) Logico-numerical max-strategy iteration. In: Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, 7737 . Springer, pp. 414-433. ISBN 9783642358739

PDF Download (254kB)

Abstract

Strategy iteration methods are used for solving fixed point equations. It has been shown that they improve precision in static analysis based on abstract interpretation and template abstract domains, e.g. intervals, octagons or template polyhedra. However, they are limited to numerical programs. In this paper, we propose a method for applying max-strategy iteration to logico-numerical programs, i.e. programs with numerical and Boolean variables, without explicitly enumerating the Boolean state space. The method is optimal in the sense that it computes the least fixed point w.r.t. the abstract domain; in particular, it does not resort to widening. Moreover, we give experimental evidence about the efficiency and precision of the approach.

Item Type:	Book Section
Keywords:	Verification, Static Analysis, Abstract Interpretation, Strategy Iteration
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 11:19
Last Modified:	09 May 2016 11:19
URI:	http://srodev.sussex.ac.uk/id/eprint/60807

View download statistics for this item

📧 Request an update