Hostname: page-component-745bb68f8f-b6zl4 Total loading time: 0 Render date: 2025-01-21T21:10:34.148Z Has data issue: false hasContentIssue false
  • English
  • Français

Programming Combinations of Deduction and BDD-based Symbolic Calculation

Published online by Cambridge University Press:  01 February 2010

Michael J. C. Gordon
Michael J. C. Gordon
Affiliation:
University of Cambridge Computer Laboratory, New Museums Site, William Gates Building, J. J. Thomson Avenue, Cambridge CB3 0FD, mjcg@cl.cam.ac.uk, http://www.cl.cam.ac.uk/~mjcg

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

A generalisation of Milner's ‘LCF approach’ is described. This allows algorithms based on binary decision diagrams (BDDs) to be programmed as derived proof rules in a calculus of representation judgements. The derivation of representation judgements becomes an LCF-style proof by defining an abstract type for judgements analogous to the LCF type of theorems. The primitive inference rules for representation judgements correspond to the operations provided by an efficient BDD package coded in C (BuDDy). Proof can combine traditional inference with steps inferring representation judgements. The resulting system provides a platform to support a tight and principled integration of theorem proving and model checking. The methods are illustrated by using them to solve all instances of a generalised Missionaries and Cannibals problem.

Type
Research Article
Information
LMS Journal of Computation and Mathematics , Volume 5 , 2002 , pp. 56 - 76
Copyright
Copyright © London Mathematical Society 2002

References

1Aagaard, Mark D., Jones, Robert B. and Seger, Carl-Johan H., ‘Lifted-FL: a pragmatic implementation of combined model checking and theorem proving’, Theorem proving in higher order logics(TPHOLs99), Lecture Notes in Comput. Sci. 1690 (Springer, 1999) 323–340.CrossRefGoogle Scholar
2Amarel, Saul, ‘On representation of problems of reasoning about action’, Machine intelligence 3 (ed. Michie, Donald, Edinburgh University Press, 1971) 131–171.Google Scholar
3Bryant, Randall E., Symbolic boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys 24 (1992) 293–318.CrossRefGoogle Scholar
4Clarke, Edmund M., Grumberg, Orna and Peled, Doron A., Model checking (The MIT Press, 1999).Google Scholar
5Coudert, Olivier, Berthet, Christian and Madre, Jean Christophe, ‘Verification of synchronous sequential machines based on symbolic execution’, Automatic verification methods for finite state systems, Lecture Notes in Comput. Sci. 407 (ed. Sifakis, J., Springer, 1989) 365–373.Google Scholar
6Gordon, Mike, ‘Reachability programming in HOL98 using BDDs’, Proc. 13th International Conference on Theorem Proving and Higher Order Logics (Springer, 2000) 179–196.CrossRefGoogle Scholar
7Gordon, Mike, ‘HolBddLib’, http://www.cl.cam.ac.uk/~mjcg/HolBddLib/.Google Scholar
8Gordon, M.J.C., Milner, R. and Wadsworth, C. P., Edinburgh LCF: a mechanised logic of computation, Lecture Notes in Comput. Sci. 78 (Springer, 1979).Google Scholar
9Harrison, John, ‘Binary decision diagrams as a HOL derived rule’, The Computer Journal 38 (1995) 162–170.CrossRefGoogle Scholar
10Hazelhurst, Scott, and Seger, Carl-Johan H., ‘Symbolic trajectory evaluation’, Formal hardware verification (ed. Kropf, Thomas, Springer, 1997) 3–78.CrossRefGoogle Scholar
11Joyce, J. and Seger, C., ‘The HOL-Voss System: model-checking inside a general-purpose theorem-prover’, Higher order logic theorem proving and its applications, 6th International Workshop, HUG'93, Vancouver, B.C., August 11–13 1993, Lecture Notes in Comput.Sci. 780 (ed. Joyce, J. J. and Seger, C.-J. H., Springer, 1994), 185’198.CrossRefGoogle Scholar
12Lee, Trevor W.S., Greenstreet, Mark R. and Seger, Carl-Johan, ‘Automatic verification of asynchronous circuits’, Tech. Rep. UBC TR 93–40, The University of British Columbia (November, 1993).Google Scholar
13McCarthy, John, ‘Elaboration tolerance’, http://www-formal.stanford.edu/jmc/elaboration/node2.html.Google Scholar
14McMillan, Kenneth L., Symbolic model checking (Kluwer Academic Publishers, 1993).CrossRefGoogle Scholar
15McMillan, K. L., ‘A compositional rule for hardware design refinement’, Computer- aided verification, CAV '97, Lecture Notes in Comput. Sci. (ed. Grumberg, Orna, Springer, Haifa, Israel, 1997) 24–35.CrossRefGoogle Scholar
16McMillan, Ken, ‘SMV’, http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/.Google Scholar
17Milner, R., ‘A theory of type polymorphism in programming’, J.Comput.SystemSci 17 (1978) 348–375.CrossRefGoogle Scholar
18O'Leary, John, Zhao, Xudong, Gerth, Robert and Seger, Carl-Johan H., ‘For mally verifying IEEE compliance of floating-point hardware’, Intel Technology J., http://developer.intel.com/technology/itj/.Google Scholar
19Rajan, S., Shankar, N. and Srivas, M. K., ‘An integration of model-checking with automated proof checking’, Computer-aided verification, CAV'95, Lecture Notes in Comput.Sci. 939 (ed. Wolper, Pierre, Springer, Liege, Belgium, 1995) 84–97.CrossRefGoogle Scholar
20Seger, Carl-Johan H., ‘VOSS - a formal hardware verification system: User's guide’, Tech. Rep UBC TR 93–45, The University of British Columbia, (December, 1993).Google Scholar
21International, Sri, ‘PVS’, http://www.csl.sri.com/pvs.html.Google Scholar