Abstract
This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of object-oriented software. It aims for integrating design, implementation, formal specification and formal verification as seamlessly as possible. The intention is to provide a platform that allows close collaboration of conventional and formal software development methods.
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
Baum, M.: A verifying debugger. Master’s thesis, Department of Computer Science, Institute for Theoretical Computer Science (to appear, 2007)
Beckert, B., Gladisch, C.: White-box testing by combining deduction-based specification extraction and black-box testing. In: Gurevich, Y. (ed.) TAP. Proceedings, International Conference on Tests and Proofs, Zürich, Switzerland. LNCS, Springer, Heidelberg (2007)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Beckert, B., Klebanov, V.: Must program verification systems and calculi be verified? In: Proceedings, 3rd International Verification Workshop (VERIFY), Workshop at Federated Logic Conferences (FLoC), Seattle, USA (2006)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer 7(3), 212–232 (2005)
Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing, vol. 74, pp. 308–312. Elsevier, Amsterdam, North-Holland (1974)
Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer’s Guide. In: Java Series, June 2000, Addison-Wesley, London, UK (2000)
Darvas, Á., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193–209. Springer, Heidelberg (2005)
Engel, C., Hähnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y. (ed.) TAP. Proceedings, International Conference on Tests and Proofs, Zürich, Switzerland. LNCS, Springer, Heidelberg (2007)
Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, New York (1996)
Giese, M.: Incremental closure of free variable tableaux. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 545–560. Springer, Heidelberg (2001)
Giese, M., Larsson, D.: Simplifying transformations of OCL constraints. In: Briand, L.C., Williams, C. (eds.) MoDELS 2005. LNCS, vol. 3713, Springer, Heidelberg (2005)
Hähnle, R., Pan, J., Rümmer, P., Walter, D.: Integration of a security type system into a program logic. In: Montanari, U., Sanella, D. (eds.) Proc. Trustworthy Global Computing, Lucca, Italy. LNCS, Springer, Heidelberg (2007)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Heisel, M., Reif, W., Stephan, W.: Program verification by symbolic execution and induction. In: Morik, K. (ed.) Proceedings, 11th German Workshop on Artificial Intelligence. Informatik Fachberichte, vol. 152, Springer, Heidelberg (1987)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)
Hunt, J.J., Jenn, E., Leriche, S., Schmitt, P., Tonin, I., Wonnemann, C.: A case study of specification and verification using JML in an avionics application. In: Rochard-Foy, M., Wellings, A. (eds.) JTRES. Proceedings, 4th Workshop on Java Technologies for Real-time and Embedded Systems, ACM Press, New York (2006)
Larsson, D., Mostowski, W.: Specifying Java Card API in OCL. In: Schmitt, P.H. (ed.) OCL 2.0 Workshop at UML 2003, vol. 102C, pp. 3–19. Elsevier, Amsterdam (2003)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual. Draft Revision 1.200 (February 2007)
Mostowski, W.: Formalisation and verification of Java Card security properties in dynamic logic. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 357–371. Springer, Heidelberg (2005)
Nanchen, S., Schmid, H., Schmitt, P., Stärk, R.F.: The ASMKeY prover. Technical Report 436, Department of Computer Science, ETH Zürich (2004)
Rümmer, P., Shah, M.A.: Proving programs incorrect using a sequent calculus for Java Dynamic Logic. In: Gurevich, Y. (ed.) TAP. Proceedings, International Conference on Tests and Proofs, Zürich, Switzerland. LNCS, Springer, Heidelberg (2007)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Stepney, S., Cooper, D., Woodcock, J.: An electronic purse: Specification, refinement, and proof. Technical monograph PRG-126, Oxford University Computing Laboratory (July 2000)
Tonin, I.: Verifying the Mondex Case Study: the KeY approach. Technical report, Department of Computer Science, Institute for Theoretical Computer Science (April 2007)
Warmer, J., Kleppe, A.: The Object Constraint Language: Getting Your Models Ready for MDA. In: Object Technology Series, August 2003, Addison-Wesley, Reading (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Ahrendt, W., Beckert, B., Hähnle, R., Schmitt, P.H. (2007). KeY: A Formal Method for Object-Oriented Systems. In: Bonsangue, M.M., Johnsen, E.B. (eds) Formal Methods for Open Object-Based Distributed Systems. FMOODS 2007. Lecture Notes in Computer Science, vol 4468. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72952-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-72952-5_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72919-8
Online ISBN: 978-3-540-72952-5
eBook Packages: Computer ScienceComputer Science (R0)