References:

1
Mark D. Aagaard , Robert B. Jones , Roope Kaivola , Katherine R. Kohatsu , Carl-Johan H. Seger, Formal verification of iterative algorithms in microprocessors, Proceedings of the 37th conference on Design automation, p.201-206, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337388]

2
Andrew Adams , Martin Dunstan , Hanne Gottliebsen , Tom Kelsey , Ursula Martin , Sam Owre, Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, p.27-42, September 03-06, 2001

3
3. Amjad H (2003) Programming a symbolic model checker in a fully expansive theorem prover. In: Basin D, Wolff B (eds) Theorem proving in higher order logics, vol. 2758 of Lecture Notes in Computer Science, Springer-Verlag, pp. 171-187.

4
David A. Basin , Stefan Friedrich , Marek Gawkowski, Verified Bytecode Model Checkers, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, p.47-66, August 20-23, 2002

5
5. Bensalem S, Ganesh V, Lakhnech Y, Munoz C, Owre S, Rueß H, Rushby J, Rusu V, Saïdi H, Shankar N, Singerman E, Tiwari A (June 2000) An overview of SAL. In: Holloway CM (ed) Fifth NASA Langley formal methods workshop, Hampton, Virginia, USA, NASA Langley Research Center, pp. 187-196.

6
Richard J. Boulton , Andrew Gordon , Michael J. C. Gordon , John Harrison , John Herbert , John Van Tassel, Experience with Embedding Hardware Description Languages in HOL, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, p.129-156, June 22-24, 1992

7
Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]

8
Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]

9
9. Buchberger B (2004) Towards the automated synthesis of a Gröbner bases algorithm. RACSAM 98(1-2):65-75.

10
10. Butterworth R, Blandford AE, Duke D (2000) Demonstrating the cognitive plausibility of interactive systems. Formal Asp Comput 12:237-259.

11
11. Byrne M, Bovair S (1997) A working memory model of a common procedural error. Cogn Sci 21(1):31-61.

12
12. Camilleri A, Gordon M, Melham T (September 1986) Hardware verification using Higher-order logic. In: Borrione D (ed) From HDL descriptions to guaranteed correct circuit designs: Proceedings of the IFIP WG 10.2 Working Conference, Grenoble, France, pp. 43-67.

13
Laurian M. Chirica , David F. Martin, Toward compiler implementation correctness proofs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.185-214, April 1986 [doi>10.1145/5397.30847]

14
Ching-Tsun Chou , Doron Peled, Formal Verification of a Partial-Order Reduction Technique for Model Checking, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.241-257, March 27-29, 1996

15
F. Corella , Z. Zhou , X. Song , M. Langevin , E. Cerny, Multiway Decision Graphs for Automated Hardware Verification, Formal Methods in System Design, v.10 n.1, p.7-46, February 1997 [doi>10.1023/A:1008663530211]

16
16. Crow J, Owre S, Rushby J, Shankar N, Srivas M (1999) A tutorial introduction to PVS. http://www.dcs.gla.ac.uk/prosper/papers.html

17
Editors:, TPHOLs 2000: Supplemental Proceedings, Oregon Graduate Institute School of Science & Engineering, 2000

18
18. Curzon P, Blandford A (June 2000) Using a verification system to reason about post-completion errors. In: Palanque P, Paternó F (eds) Participants Proceedings of DSV-IS 2000: 7th International Workshop on Design, Specification and Verification of Interactive Systems, at the 22nd International Conference on Software Engineering, Limerick, Ireland, Kluwer, pp. 293-308.

19
Paul Curzon , Ann Blandford, Detecting Multiple Classes of User Errors, Proceedings of the 8th IFIP International Conference on Engineering for Human-Computer Interaction, p.57-72, May 11-13, 2001

20
20. Curzon P, Ruksenas R, Blandford A. Formal verification in human error modelling. Submitted for publication.

21
21. Curzon P, Tahar S, Aït-Mohamed O (1998) Verification of the MDG components library in HOL. In: Grundy J, Newey M (eds) Theorem proving in higher-order logics: Emerging trends, Department of Computer Science, The Australian National University, pp. 31-46.

22
Louise A. Dennis , Graham Collins , Michael Norrish , Richard J. Boulton , Konrad Slind , Graham Robinson , Michael J. C. Gordon , Thomas F. Melham, The PROSPER Toolkit, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.78-92, March 25-April 02, 2000

23
23. Gordon MJ, Milner R, Wadsworth CP (1979) Edinburgh LCF: A mechanised logic of computation, vol. 78 of Lecture Notes in Computer Science, Springer-Verlag.

24
Michael J. C. Gordon, Reachability Programming in HOL98 Using BDDs, Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, p.179-196, August 14-18, 2000

25
M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993

26
26. Grumberg O, Katz S (March 1999) Veritech: Translating among specification and verification tools design principles, http://www.cs.technion.ac.il/labs/ssdl/research/veritech

27
J. Harrison , L. Théry, A Skeptic’s Approach to Combining HOL and Maple, Journal of Automated Reasoning, v.21 n.3, p.279-294, December 1998 [doi>10.1023/A:1006023127567]

28
Scott Hazelhurst , Carl-Johan H. Seger, Symbolic Trajectory Evaluation, Formal Hardware Verification - Methods and Systems in Comparison, p.3-78, January 1997

29
André Heck, Introduction to Maple, Springer-Verlag New York, Inc., New York, NY, 1993

30
30. Hurd J (April 1999) Integrating GANDALF and HOL. Technical Report 461, University of Cambridge, Computer Laboratory.

31
Jeffrey J. Joyce , Carl-Johan H. Seger, Linking BDD-based symbolic evaluation to interactive theorem-proving, Proceedings of the 30th international conference on Design automation, p.469-474, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164981]

32
32. Kort S, Tahar S, Curzon P (2003) Hierarchical formal verification using a hybrid tool. Softw Tools Technol Trans 4(3):313-322.

33
33. Lind-Nielsen J, BuDDY--A binary decision diagram package, http://www.itu.dk/research/buddy/

34
34. Melham T (2004) Integrating model checking and theorem proving in a reflective functional language. In: Kirchner H, Ringeissen C (eds) Integrated formal methods, vol. 2999 of Lecture Notes in Computer Science, Springer-Verlag, pp. 36-39.

35
T. Melham, Higher order logic and hardware verification, Cambridge University Press, New York, NY, 1993

36
36. Mhamdi T, Tahar S (2004) Providing automated verification in HOL using MDGs. In: Wang F (ed) Automated technology for verification and analysis, vol. 3299 of Lecture Notes in Computer Science, Springer-Verlag, pp. 278-293.

37
Laurence C. Paulson, ML for the working programmer, Cambridge University Press, New York, NY, 1991

38
S. Rajan , Natarajan Shankar , Mandayam K. Srivas, An Integration of Model Checking with Automated Proof Checking, Proceedings of the 7th International Conference on Computer Aided Verification, p.84-97, July 03-05, 1995

39
Natarajan Shankar, Combining Theorem Proving and Model Checking through Symbolic Analysis, Proceedings of the 11th International Conference on Concurrency Theory, p.1-16, August 22-25, 2000

40
Natarajan Shankar, Using Decision Procedures with a Higher-Order Logic, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, p.5-26, September 03-06, 2001

41
Sofiène Tahar , Paul Curzon , Jianping Lu, Three Approaches to Hardware Verification: HOL, MDG and VIS Compared, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.433-450, November 04-06, 1998

42
42. Tammet T (October 1997) Gandalf version c-1.0c reference manual, http://www.cs.chalmers. sr/~tammet/

43
Laurent Théry, A Machine-Checked Implementation of Buchberger's Algorithm, Journal of Automated Reasoning, v.26 n.2, p.107-137, February 2001 [doi>10.1023/A:1026518331905]

44
Tomás E. Uribe, Combinations of Model Checking and Theorem Proving, Proceedings of the Third International Workshop on Frontiers of Combining Systems, p.151-170, March 22-24, 2000

45
45. Xiong H (January 2002) Providing a formal linkage between MDG and HOL based on a verified MDG system. Ph.D. thesis, School of Computing Science, Middlesex University, UK.

46
Haiyan Xiong , Paul Curzon , Sofiène Tahar, Importing MDG Verification Results into HOL, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, p.293-310, September 01, 1999

47
Editors:, TPHOLs 2000: Supplemental Proceedings, Oregon Graduate Institute School of Science & Engineering, 2000

48
48. Xiong H, Curzon P, Tahar S, Blandford A (September 2001) Proving existential theorems when importing results from MDG to HOL. In: Boulton R, Jackson P (eds) TPHOLs 2001 Supplemental Proceedings, Informatic Research Report EDI-INF-RR-0046, pp. 384-399.

49
49. Zhou Z, Boulerice N (1996) MDG Tools (V1.0) User Manual. University of Montreal, Dept. D'IRO.

50
Z. Zhou , Xiaoyu Song , Sofiène Tahar , Eduard Cerny , Francisco Corella , Michel Langevin, Formal Verification of the Island Tunnel Controller Using Multiway Decision Graphs, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.233-247, November 06-08, 1996