Schrammel, Peter and Jeannet, Bertrand (2011) Logico-numerical abstract acceleration and application to the verification of data-flow programs. In: Static Analysis. Lecture Notes in Computer Science, 6887 . Springer, pp. 233-248.

PDF - Accepted Version Restricted to SRO admin only Download (225kB)

Abstract

Acceleration methods are commonly used for speeding up the convergence of loops in reachability analysis of counter machine models. Applying these methods to synchronous data-flow programs with Boolean and numerical variables, e.g., Lustre programs, requires the enumeration of the Boolean states in order to obtain a control flow graph (CFG) with numerical variables only. Our goal is to apply acceleration techniques to data-flow programs without resorting to this exhaustive enumeration. To this end, we present (1) logico-numerical abstract acceleration methods for CFGs with Boolean and numerical variables and (2) partitioning techniques that make logical-numerical abstract acceleration effective. Experimental results show that incorporating these methods in a verification tool based on abstract interpretation provides not only significant advantage in terms of accuracy, but also a gain in performance in comparison to standard techniques.

Item Type:	Book Section
Keywords:	Verification, Static Analysis, Abstract Interpretation, Abstract Acceleration, Control Flow Graph Partitioning
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:06
Last Modified:	09 May 2016 11:06
URI:	http://srodev.sussex.ac.uk/id/eprint/60804

View download statistics for this item

📧 Request an update