Advertisement

PROSPER An Investigation into Software Architecture for Embedded Proof Engines

  • Thomas F. Melham
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2309)

Abstract

Prosper is a recently-completed ESPRIT Framework IV research project that investigated software architectures for component-based, embedded formal verification tools. The aim of the project was to make mechanized formal analysis more accessible in practice by providing a framework for integrating formal proof tools inside other software applications. This paper is an extended abstract of an invited presentation on Prosper given at FroCoS 2002. It describes the vision of the Prosper project and provides a summary of the technical approach taken and some of the lessons learned.

Keywords

Model Checker Application Program Interface Software Architecture Theorem Prove High Order Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, ‘Combining theorem proving and trajectory evaluation in an industrial environment,’ in ACM/IEEE Design Automation Conference, Proceedings (1998), pp. 538–541.Google Scholar
  2. 2.
    M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, ‘Lifted-.: A pragmatic implementation of combined model checking and theorem proving’, in Theorem Proving in Higher Order Logics, edited by Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, Lecture Notes in Computer Science, vol. 1690 (Springer-Verlag, 1999), pp. 23–340.CrossRefGoogle Scholar
  3. 3.
    S. Agerholm, ‘Translating Specifications in VDM-SL to PVS’, in Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96: Turku, August 1996: Proceedings, edited by J. von Wright, J. Grundy, and J. Harrison Lecture Notes in Computer Science, vol. 1690 (Springer-Verlag, 1999), pp. 1–16.Google Scholar
  4. 4.
    S. Agerholm and H. Skjødt, Automating a model checker for recursive modal assertions in HOL. Technical Report DAIMI IR-92, Computer Science Department (Aarhus University, 1990).Google Scholar
  5. 5.
    W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. Hähnle, W. Menzel, and P. H. Schmitt, ‘The KeY approach: Integrating object oriented design and formal verification’, in Proceedings of the 8th European Workshop on Logics in AI (JELIA), edited by M. Ojeda-Aciego, I. P. de Guzmán, G. Brewka, and L. M. Pereira (eds.), Lecture Notes in Computer Science, vol. 1919 (Springer-Verlag, 2000), pp. 21–36Google Scholar
  6. 6.
    A. Armando, M. Kohlhase, and S. Ranise, ‘Communication protocols for mathematical services based on KQML and OMRS’, in Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium (Proceedings of the Eighth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), edited by M. Kerber and M. Kohlhase (A. K. Peters Ltd., 2001).Google Scholar
  7. 7.
    A. Armando and D. Zini, ‘Interfacing computer algebra and deduction systems via the Logic Broker Architecture’, in Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium (Proceedings of the Eighth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), edited by M. Kerber and M. Kohlhase (A. K. Peters Ltd., 2001).Google Scholar
  8. 8.
    A. Armando and D. Zini, ‘Towards Interoperable Mechanized Reasoning Systems: the Logic Broker Architecture’, in Proceedings of the AI * IA-TABOO Joint Workshop ‘Dagli Oggetti agli Agenti: Tendenze Evolutive dei Sistemi Software’, 29–30 May 2001, Parma, Italy (2001), pp. 70–75.Google Scholar
  9. 9.
    F. Baader and K. U. Schulz, eds., Frontiers of Combining Systems: First InternationalWorkshop, Munich, March 1996, Applied Logic Series, vol. 3 (Kluwer Academic Publishers, 1996).Google Scholar
  10. 10.
    L. Bening and H. Foster, Principles of Verifiable RTL Design (Kluwer, 2000).Google Scholar
  11. 11.
    S. Bensalem, V. Ganesh, Y. Lakhnech, C. Muñoz, S. Owre, H. Ruess, J. Rushby, V. Rusu, H. Saïdi, N. Shankar, E. Singerman, and A. Tiwari, ‘An overview of SAL’, in Proceedings of the Fifth NASA Langley Formal Methods Workshop, June 2000 (Williamsburg, 2000).Google Scholar
  12. 12.
    S. Bensalem, Y. Lakhnech, and S. Owre, ‘InVeSt: A tool for the verification of invariants’, in Proceedings of the 10th InternationalConfer ence on Computer Aided Verification (CAV’98), edited by A. J. Hu and M. Y. Vardi, Lecture Notes in Computer Science, vol. 1427 (Springer-Verlag, 1998), pp. 505–510.CrossRefGoogle Scholar
  13. 13.
    C. Benzmüller and V. Sorge, ‘Ω-Ants — An open approach at combining interactive and automated theorem proving’ in Symbolic Computation and Automated Reasoning: The CALCULEMUS-2000 Symposium (Proceedings of the Eighth Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), edited by M. Kerber and M. Kohlhase (A. K. Peters Ltd., 2001).Google Scholar
  14. 14.
    P. Braun, H. Lötzbeyer, B. Schätz, and O. Slotosch, ‘Consistent integration of formal methods’, in Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000: Berlin, March/April2000: Proceedings, edited by S. Graf and M. Schwartzbach, Lecture Notes in Computer Science, vol. 1785 (Springer-Verlag, 2000), pp. 48–62.CrossRefGoogle Scholar
  15. 15.
    A. Church, ‘A Formulation of the Simple Theory of Types’, Journalof Symbolic Logic, vol. 5 (1940), pp. 56–68.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri, ‘NuSMV: a new Symbolic Model Verifier’, in Proceedings of the Eleventh Conference on Computer-Aided Verification (CAV’99), edited by N. Halbwachs and D. Peled, Lecture Notes in Computer Science, vol. 1633 (Springer-Verlag, 1999), pp. 495–499.Google Scholar
  17. 17.
    A. Coglio, ‘The control component of OMRS: NQTHM as a case study’, in Proceedings of the First Workshop on Abstraction, Analogy and Metareasoning, IRST (Trento, 1996), pp. 65–71.Google Scholar
  18. 18.
    G. Collins and L. A. Dennis, ‘System description: Embedding verification into Microsoft Excel’, in Proceedings of the 17th International Conference on Automated Deduction: CADE-17, edited by D. McAllester, Lecture Notes in Artificial Intelligence, vol. 1831 (Springer-Verlag, 2000), pp. 497–501.Google Scholar
  19. 19.
    B. Colwell and B. Brennan, ‘Intel’s Formal Verification Experience on the Willamette Development’, in Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000: Portland, August2000: Proceedings, edited by M. Aagaard and J. Harrision, Lecture Notes in Computer Science, vol. 1869 (Springer-Verlag, 2000), pp. 106–107.CrossRefGoogle Scholar
  20. 20.
    B. I. Dahn, J. Gehne, T. Honigmann, and A. Wolf, ‘Integration of automated and interactive theorem proving in ILF’, in Proceedings of the 14th International Conference on Automated Deduction (CADE-14), edited by W. McCune, Lecture Notes in Artificial Intelligence, vol. 1249 (Springer-Verlag, 1997), pp. 57–60.Google Scholar
  21. 21.
    L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham, ‘The Prosper Toolkit’, in Tools and Algorithms for the Construction and Analysis of Systems: 6th International Conference, TACAS 2000: Berlin, March/April 2000: Proceedings, edited by S. Graf and M. Schwartzbach, Lecture Notes in Computer Science, vol. 1785 (Springer-Verlag, 2000), pp. 78–92. An extended version of this paper is to appear in the InternationalJournalon Software Tools for Technology Transfer.CrossRefGoogle Scholar
  22. 22.
    L. Dennis, G. Collins, R. Boulton, G. Robinson, M. Norrish, and K. Slind, The PROSPER Toolkit, version 1.4, Part of deliverable D3.5, ESPRIT LTR Project Prosper (26241), Department of Computing Science, University of Glasgow (April, 2001). Available as prosper1-4.ps.gz at http://www.dcs.gla.ac.uk/prosper/toolkit/.
  23. 23.
    D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe, Extended static checking, Research Report 159, Compaq Systems Research Center, Palo Alto (December, 1998).Google Scholar
  24. 24.
    J. Fitzgerald and P. G. Larsen, Modelling Systems: Practical Tools and Techniques in Software Development (Cambridge University Press, 1998).Google Scholar
  25. 25.
    A. Franke, S. M. Hess, C. G. Jung, M. Kohlhase, and V. Sorge, ‘Agent-Oriented Integration of Distributed Mathematical Services’, Journalof UniversalComputer Science, vol. 5 (1999), pp. 156–187.zbMATHGoogle Scholar
  26. 26.
    A. Franke and M. Kohlhase, ‘System description: MBase, an open mathematical knowledge base’, in Proceedings of the 17th InternationalConfer ence on Automated Deduction: CADE-17, edited by D. McAllester, Lecture Notes in Artificial Intelligence, vol. 1831 (Springer-Verlag, 2000), pp. 455–459.Google Scholar
  27. 27.
    D. Fuchs and J. Denzinger, Knowledge-based cooperation between theorem provers by TECHS, SEKI-Report SR-97-11 (University of Kaiserslautern, 1997).Google Scholar
  28. 28.
    D. M. Gabbay and M. de Rijke, eds., Frontiers of Combining Systems 2, Studies in Logic and Computation Series (Research Studies Press, 2000).Google Scholar
  29. 29.
    F. Giunchiglia, P. Pecchiari, and C. Talcott, ‘Reasoning theories: Towards an architecture for open mechanized reasoning systems’, in Frontiers of Combining Systems: First International Workshop, Munich, March 1996, edited by F. Baader and K. U. Schulz, Applied Logic Series, vol. 3 (Kluwer Academic Publishers, 1996), pp. 157–174.Google Scholar
  30. 30.
    M. Gordon and K. F. Larsen, Combining the Hol98 proof assistant with the BuDDy BDD package, Technical Report 481, University of Cambridge Computer Laboratory (December, 1999).Google Scholar
  31. 31.
    M. J. C. Gordon and T. F. Melham, eds., Introduction to HOL: A theorem proving environment for higher order logic (Cambridge University Press, 1993).Google Scholar
  32. 32.
    A. Holt, E. Klein, and C. Grover, ‘Natural language specifications for hardware verification’, Language and Computation, vol. 1 (2000), pp. 275–282. Special issue on ICoS-1.Google Scholar
  33. 33.
    D. W. Hoffmann and T. Kropf, ‘Automatic error correction of large circuits using boolean decomposition and abstraction’, in Correct Hardware Design and Verification Methods: 10th IFIP WG10.5 Advanced Research Working Conference: Bad Herrenalb, September 1999: Proceedings, edited by L. Pierre and T. Kropf, Lecture Notes in Computer Science, vol. 1703 (Springer-Verlag, 1999), pp. 157–171.Google Scholar
  34. 34.
    J. Hurd, ‘Integrating Gandalf and HOL’, in Theorem Proving in Higher Order Logics, edited by Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, Lecture Notes in Computer Science, vol. 1690 (Springer-Verlag, 1999), pp. 311–321.CrossRefGoogle Scholar
  35. 35.
    M. Kaufmann, P. Manolios, and J S. Moore, Computer-Aided Reasoning: An Approach (Kluwer Academic Publishers, 2000).Google Scholar
  36. 36.
    H. Kirchner and C. Ringeissen, eds., Frontiers of Combining Systems: Third InternationalWorkshop, FroCoS 2000: Nancy, March 2000: Proceedings, Lecture Notes in Artificial Intelligence, vol. 1794 (Springer-Verlag, 2000).Google Scholar
  37. 37.
    B. Krieg-Brückner, J. Peleska, E.-R. Olderog, and A. Baer, ‘The UniForM Work-Bench, a universal development environment for formal methods’, in FM’99-Formal Methods, edited by J. M. Wing, J. Woodcock, and J. Davies, vol. 2, Lecture Notes in Computer Science, vol. 1709 (Springer-Verlag, 1999), pp. 1186–1205.CrossRefGoogle Scholar
  38. 38.
    K. L. McMillan, Symbolic Model Checking (Kluwer Academic Publishers, 1993).Google Scholar
  39. 39.
    K. L. McMillan, ‘Verification of infinite state systems by compositional model checking’, in Correct Hardware Design and Verification Methods, edited by L. Pierre and T. Kropf, Lecture Notes in Computer Science, vol. 1703 (Springer-Verlag, 1999), pp. 219–233.Google Scholar
  40. 40.
    K. L. McMillan, ‘Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking’, in Correct Hardware Design and Verification Methods: 11th IFIP WG10.5 Advanced Research Working Conference, CHARME 2001: Livingston, Scotland, UK, September 4–7 2001: Proceedings, edited by T. Margaria and T. Melham, Lecture Notes in Computer Science, vol. 2144, (Springer-Verlag, 2001), pp. 179–195.Google Scholar
  41. 41.
    Microsoft Corporation, Microsoft Excel, http://www.microsoft.com/excel.
  42. 42.
    R. Milner, M. Tofte, R. Harper, and D. MacQueen, The Definition of Standard ML, revised edition (MIT Press, 1997).Google Scholar
  43. 43.
    N. Mokhoff, ‘Intel, Motorola report formal verification gains’, The EE Times Online, http://www.eetimes.com/story/OEG20010621S0080.
  44. 44.
    Object Management Group, The Common Object Request Broker: Architecture and Specification, OMG Technical Report (July 1995).Google Scholar
  45. 45.
    J. O'Leary, X. Zhao, R. Gerth, and C.-J. H. Seger, ‘Formally verifying IEEE compliance of floating-point hardware’, Intel Technology Journal (First Quarter, 1999). Available online at http://developer.intel.com/technology/itj/.
  46. 47.
    S. Rajan, N. Shankar, and M. Srivas, ‘An integration of model checking and automated proof checking’, in Proceedings of the International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, vol. 939 (Springer-Verlag, 1995), pp. 84–97.Google Scholar
  47. 48.
    K. Schneider and D. W. Hoffmann, ‘A HOL Conversion for Translating Linear Time Temporal Logic to ω-Automata’, in Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, Nice, 14–17 September, 1999, Lecture Notes in Computer Science, vol. 1690 (Springer-Verlag, 1999), pp. 255–Google Scholar
  48. 49.
    C.-J. H. Seger and R. E. Bryant, ‘Formal verification by symbolic evaluation of partially-ordered trajectories’, Formal Methods in System Design, vol. 6 (1995), pp. 147–189.CrossRefGoogle Scholar
  49. 50.
    M. Sheeran and G. Stålmarck, ‘A tutorial on Stålmarck’s proof procedure for propositional logic’, Formal Methods in System Design, vol. 16, no. 1 (2000), pp. 23–58.CrossRefGoogle Scholar
  50. 51.
    M. Staples, Linking ACL2 and HOL, Technical Report 476, University of Cambridge Computer Laboratory (1999).Google Scholar
  51. 52.
    B. Steffen, T. Margaria, and V. Braun, ‘The Electronic Tool Integration Platform: concepts and design’, International Journalon Software Tools for Technology Transfer, vol. 1 (1997), pp. 9–30.zbMATHCrossRefGoogle Scholar
  52. 53.
    A. Stevenson and L. A. Dennis, ‘Integrating SVC and HOL with the Prosper Toolkit’, in Supplemental Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2000), OGI Technical Report CSE 00-009, Oregon Graduate Institute (August, 2000), pp. 199–206.Google Scholar
  53. 54.
    T. E. Uribe, ‘Combinations of Model Checking and Theorem Proving’, in Frontiers of Combining Systems: Third InternationalWorkshop, FroCoS 2000: Nancy, March 2000: Proceedings, edited by H. Kirchner and C. Ringeissen, Lecture Notes in Artificial Intelligence, vol. 1794 (Springer-Verlag, 2000), pp. 151–170.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Thomas F. Melham
    • 1
  1. 1.Department of Computing ScienceUniversity of GlasgowGlasgowScotland

Personalised recommendations