Time: Thursday, 27.11.2003, 13.30-16.00
Place: room C3-204, Fredrik Bajersvej 7
Abstraction is fundamental in formal verification, and especially in combating the state explosion problem in model checking. Automatic techniques have been developed that eliminate presumed irrelevant detail from a model and then refine the abstraction until it is accurate enough to prove the given property. This abstraction refinement approach, initially proposed by Kurshan, has received great impulse from the use of efficient satisficabillity solvers in the check for the existence of error traces in the concrete model. Today it is widely applied to the verification of both hardware and software. For complex proofs, the challenge is to keep the abstract model small while carrying out most of the work on it. We review and contrast several refinement techniques that have been developed with this objective. These techniques differ in aspects that range from the choice of decision procedures for the various tasks, to the recourse to syntactic or semantic approaches (e.g., "moving fence" vs. predicate abstraction), and to the analysis of bundles of error traces rather than individual ones.