In this talk, I will present the fundamental results of my master's thesis. The aim of the thesis has been to verify reachability properties of timed automata using SAT-based verification methods, while mainly eliminating the state explosion problem using abstraction refinement techniques. Especially for complex and safety critical systems, reachability analysis plays a major role, thus, verification shall be restricted to the system parts essential to the property.

I will show an iterative approach to automatic verification of reachability properties. While the essential, non-abstractable system parts have to be guessed during the first cycle, from the beginning of the second cycle it is possible to acces former results and identify wrongly omitted system parts to include them again: The timed automaton and the property are firstly translated into formulae, such that abstraction reduces to modification of formulae and these may be verified using a SAT-based model checker. Identification of wrongly omitted system parts and subsequent refinement are realised using craig interpolants resulting from false negatives.