Login | Register

Integrating SAT with MDG for Efficient Invariant Checking


Integrating SAT with MDG for Efficient Invariant Checking

Hoque, Khaza Anuarul (2011) Integrating SAT with MDG for Efficient Invariant Checking. Masters thesis, Concordia University.

[thumbnail of Hoque_MASc_S2011.pdf]
Text (application/pdf)
Hoque_MASc_S2011.pdf - Accepted Version


Multiway Decision Graph (MDG) is a canonical representation of a subset of many-sorted first-order logic. It generalizes the logic of equality with abstract types and uninterpreted function symbols. The area of Satisfiability (SAT) has been the subject of intensive research in recent years, with significant theoretical and practical contributions. From a practical perspective, a large number of very effective SAT solvers have recently been proposed, most of which based on improvements made to the original Davis-Putnam algorithm. Local search algorithms have allowed solving extremely large satisfiable instances of SAT. The combination between various verification methodologies will enhance the capabilities of each and overcome their limitations. In this thesis, we introduce a methodology and propose a new design verification tool integrating MDG and SAT, to check the safety of a design by invariant checking. Using MDG to encode the set of states provide powerful mean of abstraction. We use SAT solver searching for paths of reachable states violating the property under certain encoding constraints. In addition, we also introduce an automated conversion-verification methodology to convert a Directed Formula (DF) into Conjunctive Normal Form (CNF) formula that can be fed to a SAT solver. The formal verification of this conversion is conducted within the HOL theorem prover. Finally, we implement and conduct experiment on some examples along with a case study to show the correctness and the efficiency of our approach.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Hoque, Khaza Anuarul
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:28 March 2011
Thesis Supervisor(s):Mohamed, Otmane Ait
ID Code:7171
Deposited On:08 Jun 2011 19:00
Last Modified:18 Jan 2018 17:30
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