Login | Register

On the embedding of multiway decision graphs in HOL


On the embedding of multiway decision graphs in HOL

Mhamdi, Tarek (2003) On the embedding of multiway decision graphs in HOL. Masters thesis, Concordia University.

[thumbnail of MQ83872.pdf]
Text (application/pdf)


The increasing complexity of hardware systems requires more and more sophisticated methods of verification. While model checking suffers from the state space explosion problem, theorem proving is quite tedious and impractical for verifying complex designs. In this thesis, we propose 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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Mhamdi, Tarek
Pagination:xii, 93 leaves ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Tahar, Sofiene
Identification Number:QA 76.9 A96M43 2003
ID Code:2278
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:26
Last Modified:13 Jul 2020 19:51
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top