R3 develops methodologies for directed model checking using heuristic search. Building on ideas originating in artificial intelligence search and in particular planning, the project was able to accelerate directed model checking of timed systems significantly. In the coming phase of AVACS we intend to concentrate on developing new admissible heuristics in order to support the generation of shortest error traces. Further, we will apply the developed methods also to correctness proofs and to system classes going beyond timed systems.