Software Model Checking Using Linear Constraints

Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. In this context Boolean programs are commonly employed as simple, yet useful ions from conventional programming languages. In this paper se Linear Programs as a finer grained abstraction for sequential programs and propose a model checking procedure for this family of programs. We also present the eureka toolkit, which consists of a prototype implementation of our model checking procedure for Linear Programs as well as of a library of Linear Programs to be used for benchmarking. Experimental results obtained by running our model checker against the library provide evidence of the effectiveness of the approach.

• Type: Conference
• Year: 2004
• Where: ICFEM
• Authors: Alessandro Armando, Claudio Castellini, Jacopo Mantovani
• Keywords: ICFEM 2004, Linear Programs, Model Checking, Model Checking Procedure