Abstract
The Prosper (Proof and Specification Assisted Design Environments) project advocates the use of toolkits which allow existing verification tools to be adapted to a more flexible format so that they may be treated as components. A system incorporating such tools becomes another component that can be embedded in an application.
This paper describes the Prosper Toolkit which enables this. The nature of communication between components is specified in a language-independent way. It is implemented in several common programming languages to allow a wide variety of tools to have access to the toolkit.
Work funded by ESPRIT Framework IV Grant LTR 26241
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
M. D. Aagaard, R. B. Jones, and C.-J. H. Seger, Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. Y. Bertot, G. Dowek, A. Hirshowitz, C. Paulin and L. Théry (eds), Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1690, Springer-Verlag, pp. 323–340, 1999. 89
C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, A. Meirer, E. Melis, W. Schaarschmidt, J. Siekmann, and V. Sorge, ΩMEGA, Towards a mathematical assistant. 14th Conference on Automated Deduction, W. McCune (ed), Lecture Notes in Artificial Intelligence 1249, Springer-Verlag, pp. 252–255, 1997. 89
R. Boulton, K. Slind, A. Bundy, and M. Gordon, An interface between CLAM and HOL. J. Grundy and M. Newey (eds), Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1479, Springer-Verlag, pp. 87–104, 1998. 89
B. Brock, M. Kaufmann, and J Moore, ACL2 Theorems about Commercial Microprocessors. M. Srivas and A. Camilleri (eds), Proceedings of Formal Methods in Computer-Aided Design (FMCAD’96), Springer-Verlag, pp. 275–293, 1996. 83, 90
A. Bundy, F. van Harmelen, C. Horn, and A. Smaill, The Oyster-Clam system. 10th International Conference on Automated Deduction, M. E. Stickel (ed), Lecture Notes in Artificial Intelligence 449, Springer-Verlag, pp. 647–648, 1990. 89
A. Church, A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic, vol. 5, pp. 56–68, 1940. 80, 82
A. Coglio, The Control Component of OMRS: NQTHM as a Case Study. Extended abstract in Proceedings of the First Workshop on Abstraction, Analogy and Metareasoning, IRST, Trento, Italy, pp. 65–71, 1996. 90
J. Fitzgerald and P. G. Larsen, Modelling Systems: Practical Tools and Techniques in Software Development, Cambridge University Press, 1998. 80
A. Franke, S. M. Hess, C. G. Jung, M. Kohlhase, and V. Sorge, Agent-Oriented Integration of Distributed Mathematical Services. Journal of Universal Computer Science, 5(3), pp. 156–187, 1999. 89
J. A. Goguen and Luqi, Formal methods and social context in software development. Proceedings TAPSOFT’95, Lecture Notes in Computer Science 915. Springer-Verlag, pp. 62–81, 1995. 78
M. J. C. Gordon and T. F. Melham (eds), Introduction to HOL: A theorem proving environment for higher order logic, Cambridge University Press, 1993. 79
F. Giunchiglia, P. Pecchiari, and C. Talcott, Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. F. Baader and K. U. Schulz (eds), Frontiers of Combining Systems-First International Workshop (FroCoS’96), Kluwer’s Applied Logic Series (APLS), pp. 157–174, 1996. 90
A. Holt and E. Klein, A semantically-derived subset of English for hardware verification. 37th Annual Meeting of the Association for Computational Linguistics: Proceedings of the Conference, Association for Computational Linguistics, pp. 451–456, 1999. 85
J. Hurd, Integrating Gandalf and HOL. Y. Bertot, G. Dowek, A. Hirshowitz, C. Paulin and L. Théry (eds). Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1690, Springer-Verlag, pp. 311–321, 1999. 83
J. Joyce and C.-J. Seger, Linking BDD based symbolic evaluation to interactive theorem proving. ACM/IEEE Design Automation Conference, June 1993. 89
B. Kreig-Brükner, J. Peleska, E.-R. Olderog, and A. Baer, The UniForM Work-Bench, a Universal Development Environment for Formal Methods. J. M. Wing, J. Woodcock and J. Davies (eds), FM’99-Formal Methods, vol. 2, Lecture Notes in Computer Science 1709, pp. 1186–1205, 1999. 90
K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers. 1993. 83
Microsoft Corporation, Microsoft Excel, http://www.microsoft.com/excel. 87
R. Milner, M. Tofte, R. Harper and D. MacQueen, The Definition of Standard ML (Revised), MIT Press, 1997. 80
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. Online at http://developer.intel.com/technology/itj/. 89
S. Rajan, N. Shankar, and M. Srivas, An integration of model checking and automatedpro of checking. International Conference on Computer-Aided Verification, Lecture Notes in Computer Science 939, Springer-Verlag, pp. 84–97, 1995. 89
M. Sheeran and G. Stålmarck, A tutorial on Stålmarck’s proof procedure for propositional logic. The Second International Conference on Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 1522, Springer-Verlag, pp. 82–99, 1998. 83, 88
G. Stålmarck and M. Säflund, Modelling and Verifying Systems and Software in Propositional Logic. Proceedings of SAFECOMP’ 90, Pergamon Press, pp. 31–36, 1990. 83, 88
B. Steffen, T. Margaria, and V. Braun, The Electronic Tool Integration Platform: concepts and design. International Journal on Software Tools for Technology Transfer, 1(1 + 2), pp. 9–30, 1997. 89
T. Tammet, A resolution theorem prover for intuitionistic logic. 13th International Conference on Automated Deduction, Lecture Notes in Computer Science 1104, Springer-Verlag, pp. 2–16, 1996. 83
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dennis, L.A. et al. (2000). The PROSPER Toolkit. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_7
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive