MDG-SAT: an automated methodology for efficient safety checking

Hoque, Khaza Anuarul; Mohamed, Otmane Ait; Abed, Sa'ed et Boukadoum, Mounir (2012). « MDG-SAT: an automated methodology for efficient safety checking ». International Journal of Critical Computer-Based Systems, 3(1/2), pp. 4-25.

Fichier(s) associé(s) à ce document :
Télécharger (398kB)


Multiway decision graph (MDG) is a canonical representation of a subset of many-sorted first-order logic. It generalises 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. In this paper, we 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 provides a powerful mean of abstraction. We use a SAT solver to search for paths of reachable states violating the property under certain encoding constraints. In addition, we introduce an automated conversion-verification methodology to convert a directed formula (DF) into a 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 present experimental results and a case study to show the correctness and the efficiency of our proposed methodology.

Type: Article de revue scientifique
Mots-clés ou Sujets: satisfiability; SAT; invariant checking; model checking; multiway decision graph; MDG; CNF conversion.
Unité d'appartenance: Faculté des sciences > Département d'informatique
Déposé par: A. Mounir Boukadoum
Date de dépôt: 15 avr. 2016 13:05
Dernière modification: 27 avr. 2016 18:07
Adresse URL :


Voir les statistiques sur cinq ans...