Members

• Tarek El Mhamdi
• Sofiène Tahar

External Collaborators

• HVG group in Cambridge

Description

In this project, we propose to develop an embedding of MDG data structure and basic and operations (such as conjunction) in HOL. The idea is to enable a user to write a HOL term in a similar MDG underlying first-order logic, which will be passed to the MDG package for analyses and further manipulation as an MDG data structure. This will enable the use of MDGs operations, rather than proof tactics, from HOL, hence MDG will become a decision procedure, transparent to the user. MDGs in HOL will give an alternate, often easier, method for showing functional equivalence of first-order equations.

Once HOL terms are represented as MDGs and MDG algorithms accessible, it will allow an automatic verification of specific HOL goals. A related work was done by K. Larsen at Cambridge U. It consisted of embedding a BDD package, called BuDDy into HOL. Hence, any Boolean term with Boolean free variables can be represented by a BDD. The BuDDy package has been interfaced to ML (underlying language of HOL) so that BDDs can be implemented as ML values of a type bdd and the various BuDDy operations are linked to ML functions.

Similarly, we think that an interface to MDG should provide an ML type mdg together with ML functions corresponding to the functions in the MDG package. Using these, it will be possible to implement a function that maps any quantified first-order formula to an MDG.

Publications

1. T. Mhamdi and S. Tahar: Providing Automated Verification in HOL using MDGs; In: F. Wang (Ed.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 3299, Springer Verlag, 2004, pp. 278-293. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Taiwan, November 2004]
2. T. Mhamdi and S. Tahar: Embedding Multiway Decision Graphs in HOL; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'04), Park City, Utah, USA, September 2004, pp. 121-136.
3. T. Mhamdi, and S. Tahar: Embedding Multiway Decision Graphs in HOL; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2004.
4. T. El-Mhamdi: On the Embedding of Multiway Decision Graphs in HOL. MaSc Thesis, Concordia University, Department of Electrical and Computer Engineering, August 2003.