Skip to main content
SpringerLink
Log in

An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs

  • Regular Paper
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

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 Binary Decision Diagrams (ROBDDs) to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae (DF). Then, the MDGs operations are defined and the correctness proof of each operation is provided. The MDG reachability algorithm is then defined as a conversion that uses our MDG theory within HOL. Finally, a set of experimentations over benchmark circuits has been conducted to ensure the applicability and to measure the performance of our approach.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Kropf T. Introduction to Formal Hardware Verification. Springer Verlag, 1999.

  2. Aagaard M D, Jones R B, Seger C H. Combining theorem proving and trajectory evaluation in an industrial environment. In Proc. the 1998 Conference on Design Automation (DAC-98), Los Alamitos, CA, ACM/IEEE, Jun. 1998, pp.538–541.

  3. Joyce J J, Seger C H (eds.). The HOL-Voss system: Model checking inside a general-purpose theorem prover. Lecture Notes in Computer Science 780, Springer, 1994, pp.185–198.

  4. Schneider K, Kropf T. Verifying hardware correctness by combining theorem proving and model checking. Technical Report SFB 358-C2-5/95, Institut für Rechnerentwurf und Fehlertoleranz, 1995.

  5. Kort S, Tahar S, Curzon P. Hierarchical verification using an MDG-HOL hybrid tool. International Journal on Software Tools for Technology Transfer, May 2003, 4(3): 313–322.

    Article  Google Scholar 

  6. Mizouni R, Tahar S, Curzon P. Hybrid verification incorporating HOL theorem proving and MDG model checking. Microelectronics Journal, November 2006, 37(11): 1200–1207.

    Article  Google Scholar 

  7. Rajan S, Shankar N, Srivas M K. An integration of model checking with automated proof checking. In Proc. the 7th International Conference on Computer Aided Verification, Wolper P (ed.), Liege, Belgium, LNCS 939, Springer Verlag, 1995, pp.84–97.

  8. Schneider K, Hoffmann D. A HOL conversion for translating linear time temporal logic to ω-automata. In Proc. TPHOLs, Nice, France, LNCS 1690, Springer-Verlag, 1999, pp.255–272.

  9. Amjad H. Programming a symbolic model checker in a fully expansive theorem prover. In Proc. the 16th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 2758, Springer-Verlag, 2003, pp.171–187.

  10. Gordon M J C. Programming combinations of deduction and BDD-based symbolic calculation. LMS Journal of Computation and Mathematics, Aug. 2002, ISSN 1461-1570, 5: 56–76.

  11. Gordon M J C. Reachability programming in HOL98 using BDDs. In Proc. International Conference on Theorem Proving in Higher Order Logics (TPHOLs), Portland, USA, Lecture Notes in Computer Science, August 14–18, 2000, pp.179–196.

  12. Seger C H. Voss — A formal hardware verification system, user’s guide. Technical report, Nortel Networks, Ottawa, Canada, The University of British Columbia, December, 1993.

  13. Corella F, Zhou X, Song X, Langevin M, Cerny E. Multiway decision graphs for automated hardware verification. Formal Methods in System Design, February 1997, 10(1): 7–46.

    Article  Google Scholar 

  14. Cadence Design Systems. V2.3. FormalCheck Users Guide, August 1999.

  15. McMillan K L. Symbolic Model Checking. Kluwer Academic Publishers, Boston, Massachusetts, 1993.

    MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

  17. Aagaard M, Jones R B, Kaivola R, Kohatsu K R, Seger C H. Formal verification of iterative algorithms in microprocessors. In Proc. the 37th Conference on Design Automation (DCA‘00), Los Angeles, California, USA, ACM, 2000, pp.201–206.

  18. Melham T. Integrating model checking and theorem proving in a reflective functional language. In Proc. Integrated Formal Methods: 4th International Conference (IFM 2004), Boiten E A, Derrick J, Smith G (eds.), Canterbury, UK, Lecture Notes in Computer Science 2009, Springer-Verlag, April 4–7, 2004, pp.36–39.

  19. John Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 1995, 38: 162–170.

    Article  MathSciNet  Google Scholar 

  20. Pisini V, Tahar S, Curzon P, Ait-Mohamed O, Song X. Formal hardware verification by integrating HOL and MDG. In Proc. IEEE GLS-VLSI’00, Chicago, Illinois, USA, 2000, pp.23–28.

  21. Mhamdi T, Tahar S. Providing automated verification in HOL using MDGs. In Proc. Automated Technology for Verification and Analysis, National Taiwan Univ., Taiwan, China, 2004, pp.278–293.

  22. Xiong H, Curzon P, Tahar S, Blandford A. Providing a formal linkage between MDG and HOL. Formal Methods in Systems Design, 2006, 29(3): 1–36.

    Google Scholar 

  23. Reif W, Ruf J, Schellhorn G, Vollmer T. Do you trust your model checker? In Proc. Formal Methods in Computer Aided Design (FMCAD), Warren A Hunt Jr, Steven D Johnson (eds.), LNCS 1954, Springer, November 2000, pp.199–216.

  24. Gordon M J C, Melham T F (eds.) Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York, NY, USA, 1993.

    MATH  Google Scholar 

  25. Crow J, Owre S, Rushby J, Shankar N, Srivas M. A tutorial introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, USA, 1995.

  26. Huet G, Kahn G, Paulin-Mohring C. The Coq Proof Assistant: A Tutorial. HAL-CCSd-CNRS, 2002.

  27. Matt Kaufmann, Panagiotis Manolios, J Strother Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Jun. 2000.

  28. Verma K N, Goubault-Larrecq J, Prasad S, Arun-Kumar S. Reflecting BDDs in Coq. In Proc. 6th Asian Computing Science Conference (ASIAN‘2000), Penang, Malaysia, Nov. 2000, LNCS 1961, Springer, 2000, pp.162–181.

  29. Ortner V, Schirmer N. Verification of BDD Normalization. In Proc. TPHOLs, Oxford, UK, 2005, pp.261–277.

  30. S Abed, O Ait Mohamed, G Al Sammane. On the integration of decision diagrams in high order logic based theorem provers: A survey, Journal of Computer Science, 2007, 10(3): 810–817.

    Google Scholar 

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

    Article  MATH  Google Scholar 

  32. Clocksin W, Mellish C. Programming in Prolog. Springer Verlag, 1987.

  33. Zhou Z, Boulerice N. MDGs tools (V1.0) user’s manual. D’IRO, University of Montreal, June 1996.

  34. Gordon M, Milner R, Wadsworth C. Edinburgh LCF. Lecture Notes in Computer Science 78, Springer Verlag, 1979.

  35. Gordon M. From LCF to HOL: A Short History. Proof, Language, and Interaction: Essays in Honour of Robin Milner, Cambridge: MIT Press, MA, USA, 2000, pp.169–185.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  37. S Abed, O Ait Mohamed. Embedding of MDG directed formulae in HOL theorem prover. In Proc. 9th Maghrebian Conference on Software Engineering and Artificial Intelligence (MCSEAI‘06), Agadir, Morocco, December 2006, pp.659–664.

  38. S Abed, O Ait Mohamed, G Al Sammane. A high level reachability analysis using multiway decision graphs in the HOL theorem prover. In B-Track Proc. International Conference on Theorem Proving in Higher Order Logics (TPHOLs‘07), Kaiserslautern, Germany, September 2007, pp.1–17.

  39. S Abed, O Ait Mohamed, G Al Sammane. Reachability analysis using multiway decision graphs in the HOL theorem prover. In Proc. ACM SAC’08, Brazil, ACM Press, 2008, pp.333–338.

  40. S Abed, O Ait Mohamed, G Al Sammane. On the embedding and verification of multiway decision graphs in HOL theorem prover. Technical Report 2007-1-Abed, ECE Department, Concordia University, Montreal, Canada, February 2007.

  41. Abed S. Verification of MDG algorithms. http://www.ece.concordia.ca/~s_abed/Project.htm.

  42. Butler R W. An introduction to requirements capture using PVS: Specification of a simple autopilot. Technical report, NASA Technical Memorandum 110255, NASA Langley Research, 1996.

  43. Young W. The specification of a simple autopilot in ACL. Technical Report CLI Internal Note 327, July 1996.

  44. Network Processing Forum. Look-Aside (LA-1) Interface, Implementation Agreement, Revision 1.1. Kluwer Academic Publishers, April 15, 2004.

  45. Zhou Z, Song X, Tahar S, Cerny E, Corella F, Langevin M. Formal verification of the island tunnel controller using multiway decision graphs. In Proc. the First International Conference on Formal Methods in Computer-Aided Design (FMCAD‘96), London, UK, Springer-Verlag, 1996, pp.233–247.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ECE Department, Concordia University, Montreal, Canada

    Sa’ed Abed, Otmane Ait Mohamed & Ghiath Al-Sammane

Authors
  1. Sa’ed Abed
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Otmane Ait Mohamed
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ghiath Al-Sammane
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sa’ed Abed.

Electronic Supplementary Material

Below is the link to the electronic supplementary material.

(PDF 76.7 kb)

Rights and permissions

Reprints and permissions

About this article

Cite this article

Abed, S., Ait Mohamed, O. & Al-Sammane, G. An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs. J. Comput. Sci. Technol. 24, 76–95 (2009). https://doi.org/10.1007/s11390-009-9205-8

Download citation

  • Received:

  • Revised:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11390-009-9205-8

Keywords

Search

Navigation