research-article

Reachability analysis using multiway decision graphs in the HOL theorem prover

Authors:

Sa'ed Abed,

Otmane Ait Mohamed,

Ghiath Al SammaneAuthors Info & Claims

SAC '08: Proceedings of the 2008 ACM symposium on Applied computing

Pages 333 - 338

https://doi.org/10.1145/1363686.1363774

Published: 16 March 2008 Publication History

Get Access

Abstract

In this paper, all the necessary infrastructure is provided to define a state exploration approach within the HOL theorem prover. While related work has tackled the same problem by representing primitive Binary Decision Diagram (BDD) operations as inference rules added to the core of the theorem prover, the presented approach is based on the Multiway Decision Graphs (MDGs). MDG generalizes BDD to represent and manipulate a subset of first-order logic formulae. Considering MDG instead of BDD will raise the abstraction level of what can be verified using states exploration within a theorem prover. A canonic MDGs is defined in HOL as well-formed directed formulae. Then, the basic MDG operations is formalized following a deep embedding approach and the correctness proof for each operation is derived. Finally, the reachability analysis is implemented as a tactic that uses the MDG theory within HOL.

References

[1]

Verification of MDG using HOL theorem prover. http://users.encs.concordia.ca/~ait/MDG-HOL.htm.

Google Scholar

[2]

S. Abed and O. A. Mohamed. Embedding of MDG directed formulae in HOL theorem prover. In Proc. of the 9th MCSEAI'06, pages 659--664, December 2006.

Google Scholar

[3]

O. Ait-Mohamed, X. Song, and E. Cerny. On the non-termination of MDG-based abstract state enumeration. Theoretical Computer Science, 300:161--179, 2003.

Digital Library

Google Scholar

[4]

H. Amjad. Programming a symbolic model checker in a fully expansive theorem prover. In Proc. of the 16th TPHOLs, volume 2758 of LNCS, pages 171--187. Springer-Verlag, 2003.

Google Scholar

[5]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677--691, August 1986.

Digital Library

Google Scholar

[6]

F. Corella, Z. Zhou, X. Song, M. Langevin, and E. Cerny. Multiway decision graphs for automated hardware verification. In Formal Methods in System Design, volume 10, pages 7--46, February 1997.

Digital Library

Google Scholar

[7]

M. Gordon. Reachability programming in HOL98 using BDDs. In TPHOLs, pages 179--196, 2000.

Digital Library

Google Scholar

[8]

M. Gordon. Programming combinations of deduction and BDD-based symbolic calculation. LMS Journal of Computation and Mathematics, 5:56--76, Aug. 2002.

Crossref

Google Scholar

[9]

J. Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162--170, 1995.

Crossref

Google Scholar

[10]

S. Kort, S. Tahar, and P. Curzon. Hierarchal verification using an MDG-HOL hybrid tool. STTT, 4(3):313--322, May 2003.

Crossref

Google Scholar

[11]

T. Mhamdi and S. Tahar. Providing automated verification in HOL using MDGs. In ATVA, pages 278--293, 2004.

Crossref

Google Scholar

[12]

V. Ortner and N. Schirmer. Verification of BDD normalization. In TPHOLs, pages 261--277, 2005.

Digital Library

Google Scholar

[13]

K. N. Verma, J. Goubault-Larrecq, S. Prasad, and S. Arun-Kumar. Reflecting BDDs in Coq. In Proc. of the 6th ASIAN'2000, Penang, Malaysia, Nov. 2000, volume 1961, pages 162--181. Springer-Verlag, 2000.

Digital Library

Google Scholar

[14]

Y. Xu, X. Song, E. Cerny, and O. A. Mohamed. Model checking for a first-order temporal logic using multiway decision graphs (MDGs). The Computer Journal, 47(1):71--84, 2004.

Crossref

Google Scholar

Cited By

View all

Mitra SGhosh PDasgupta P(2012)Verification by parts: reusing component invariant checking resultsIET Computers & Digital Techniques10.1049/iet-cdt.2010.00486:1(19)Online publication date: 2012
https://doi.org/10.1049/iet-cdt.2010.0048
Hoque KMohamed OAbed SBoukadoum M(2010)SAT based model checking for MDG modelsProceedings of the 8th IEEE International NEWCAS Conference 201010.1109/NEWCAS.2010.5603785(241-244)Online publication date: Jun-2010
https://doi.org/10.1109/NEWCAS.2010.5603785
Abed SAit Mohamed O(2009)LCF-style Platform based on Multiway Decision GraphsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2009.07.012246(3-26)Online publication date: 1-Aug-2009
https://dl.acm.org/doi/10.1016/j.entcs.2009.07.012
Show More Cited By

Index Terms

Reachability analysis using multiway decision graphs in the HOL theorem prover

Recommendations

An abstract reachability approach by combining HOL induction and multiway decision graphs

In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs (MDGs) theory in HOL. MDGs generalize Reduced Ordered ...
Multiway decision graphs reduction approach based on the HOL theorem prover
VECoS'08: Proceedings of the Second international conference on Verification and Evaluation of Computer and Communication Systems

Multiway Decision Graphs (MDGs) subsume Binary Decision Diagrams (BDDs) by representing formulae which are suitable for first-order model checking able to handle large datapath circuits. In this paper, we propose a reduction approach to improve MDGs ...
MDGs Reduction Technique Based on the HOL Theorem Prover
ISMVL '10: Proceedings of the 2010 40th IEEE International Symposium on Multiple-Valued Logic

Multiway Decision Graphs (MDGs) subsume Binary Decision Diagrams(BDDs) and extend them by a first-order formulae suitable for model checking of data path circuits. In this paper, we propose a reduction technique to improve MDGs model checking. We use a ...

Comments

Information & Contributors

Information

Published In

SAC '08: Proceedings of the 2008 ACM symposium on Applied computing

March 2008

2586 pages

ISBN:9781595937537

DOI:10.1145/1363686

Conference Chairs:
Roger L. Wainwright
University of Tulsa
,
Hisham M. Haddad
Kennesaw State University

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 March 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAC '08

Sponsor:

SIGAPP

SAC '08: The 2008 ACM Symposium on Applied Computing

March 16 - 20, 2008

Fortaleza, Ceara, Brazil

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
124
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Mitra SGhosh PDasgupta P(2012)Verification by parts: reusing component invariant checking resultsIET Computers & Digital Techniques10.1049/iet-cdt.2010.00486:1(19)Online publication date: 2012
https://doi.org/10.1049/iet-cdt.2010.0048
Hoque KMohamed OAbed SBoukadoum M(2010)SAT based model checking for MDG modelsProceedings of the 8th IEEE International NEWCAS Conference 201010.1109/NEWCAS.2010.5603785(241-244)Online publication date: Jun-2010
https://doi.org/10.1109/NEWCAS.2010.5603785
Abed SAit Mohamed O(2009)LCF-style Platform based on Multiway Decision GraphsElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2009.07.012246(3-26)Online publication date: 1-Aug-2009
https://dl.acm.org/doi/10.1016/j.entcs.2009.07.012
Abed SMohamed OAl-Sammane G(2009)An abstract reachability approach by combining HOL induction and multiway decision graphsJournal of Computer Science and Technology10.1007/s11390-009-9205-824:1(76-95)Online publication date: 1-Jan-2009
https://dl.acm.org/doi/10.1007/s11390-009-9205-8
Abed SMohamed OSammane G(2008)The performance of combining multiway decision graphs and HOL theorem prover2008 Forum on Specification, Verification and Design Languages10.1109/FDL.2008.4641435(136-141)Online publication date: Sep-2008
https://doi.org/10.1109/FDL.2008.4641435

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

An abstract reachability approach by combining HOL induction and multiway decision graphs

Multiway decision graphs reduction approach based on the HOL theorem prover

MDGs Reduction Technique Based on the HOL Theorem Prover

Comments

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Other Metrics

Article Metrics

Other Metrics

Cited By

Login options

Full Access

PDF

eReader

Abstract

References

Cited By

Index Terms

Recommendations

An abstract reachability approach by combining HOL induction and multiway decision graphs

Multiway decision graphs reduction approach based on the HOL theorem prover

MDGs Reduction Technique Based on the HOL Theorem Prover

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Get Access

Login options

Full Access

View options

PDF

eReader

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations