9.7 Concluding remarks 563 logic (HOL) system [Joyce 1993]. A proposal called interface logics [Guttman 1991] discusses the idea of combining different theorem provers by defining a single logic such that the logic of each individual tool can be viewed as its sub- logics. [Jang 1997] used CTL model checking to verify a set of properties of embedded microcontrollers, and the proof of the top-level specification was achieved through a compositional argument by use of the properties instead of through a theorem prover. A hybrid of two model-checking techniques, called MIST [Hazelhurst 2002], enables a handshake between symbolic trajec- tory evaluation and symbolic model checking. Generally speaking, hybrid methods combining formal and informal tech- niques aim to increase the design space coverage and, thus, the probability of finding design errors. These types of methods include control space explora- tion, directed functional test generation, combining ATPG with formal tech- niques, and heuristic-based traversal. Control space exploration addresses the problem of finding bugs and increases space coverage by exploring control logic [Iwashita 1994; Ho 1995; Geist 1996; Moondanos 1998]. Directed func- tional test generation leverages the strengths of both formal verification and sim- ulation techniques to generate functional tests [Sumners 2000; Ganai 2001; Mishra 2005]. Because ATPG can avoid state space explosion by use of dual jus-