Static Analysis using Parameterised Boolean Equation Systems

The well-known problem of state space explosion in model checking is even more critical when applying this technique to programming languages, mainly due to the presence of complex data structures. One recent and promising approach to deal with this problem is the conn of an abstract and correct representation of the global program state allowing to match visited states during program model exploration. cular, one powerful method to implement abstract matching is to fill the state vector with a minimal amount of relevant variables for each program point. In this paper, we combine the on-the-fly model-checking approach (incremental construction of the program state space) and the static analysis method called influence analysis (extraction of significant variables for each program point) in order to automatically construct act matching function. Firstly, we describe the problem as an alternation-free value-based

• Type: Journal
• Year: 2006
• Where: CORR
• Authors: María-del-Mar Gallardo, Christophe Joubert, Pedro Merino
• Keywords: Abstract Matching, CORR 2006, Education, Program State, State Space