Sciweavers

ENTCS
2006

Model Checking Linear Programs with Arrays

13 years 3 months ago
Model Checking Linear Programs with Arrays
In previous work we proposed Linear Programs as a fine grained model for imperative programs, and showed how the model checking procedure used in SLAM can be generalised to a model checking procedure for Linear Programs. In this paper we show that our model checking procedure for linear programs can be extended in such a way to support the analysis of linear programs featuring a symbol for undefined values and conditional expressions. This extension is particularly important as it paves the way to the construction of model checking procedures for wider classes of imperative programs such as, e.g., linear programs with arrays. We provide a detailed account of a symbolic model checking procedure for this extended class of linear programs, discuss its implementation in the eureka tool, and present experimental results that confirm its effectiveness in the analysis of linear programs with arrays.
Alessandro Armando, Massimo Benerecetti, Jacopo Ma
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Alessandro Armando, Massimo Benerecetti, Jacopo Mantovani
Comments (0)