- While model checking suffers from the state space explosion problem, theorem
proving is quite tedious and impractical for verifying complex designs. In
this work, we present a verification framework in which we attempt to strike
the balance between the expressiveness of theorem proving and the efficiency
and automation of state exploration techniques. To this end, we propose to
integrate a layer of checking algorithms based on Multiway Decision Graphs (MDG)
in the HOL theorem prover. We embedded the MDG underlying logic in HOL and
implemented a platform that provides a set of algorithms allowing the user to
develop his/her own state-exploration based application inside HOL. While the
verification problem is specified in HOL, the proof is derived by tightly
combining the MDG based computations and the theorem prover facilities. We
have been able to implement different state exploration techniques within HOL
such as MDG reachability analysis, equivalence and model checking.
 Download
PDF file (PDF
File) |
| Download
postscript file (PS
File) |
| Send comments
and suggestions to: tahar@ece.concordia.ca |