Set-Based Analysis of Reactive Infinite-state Systems

We present an automated abstract verification method for infinite-state systems specified by logic programs (which are a uniform and intermediate layer to which diverse formalisms such as transition systems, pushdown processes and while programs can be mapped). \linebreak We establish connections between: logic program semantics and CTL properties, set-based program analysis and pushdown processes, and also between model checking and constraint solving, viz.\ theorem proving. \linebreak We show that set-based analysis can be used to compute supersets of the values of program variables in the states that satisfy a given CTL property