This chapter gives a systematic tutorial introduction on how to perform formal program verification with the KeY system. It illustrates a number of complications and pitfalls, notably programs with loops, and shows how to deal with them. After working through this tutorial, you should be able to formally verify with KeY the correctness of simple Java programs, such as standard sorting algorithms, gcd, etc. This chapter is intended to be read with a computer at hand on which the KeY system is up and running, so that every example can be tried out immediately. The KeY system, specifically its version 2.6 used in this book, is available for download from www.key-project.org. The example input files can be found on the web page for this book, www.key-project.org/thebook2, as well as in the examples directory of your KeY system’s installation
CITATION STYLE
Beckert, B., Hähnle, R., Hentschel, M., & Schmitt, P. H. (2016). Formal verification with KeY: A tutorial. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10001 LNCS, pp. 541–570). Springer Verlag. https://doi.org/10.1007/978-3-319-49812-6_16
Mendeley helps you to discover research relevant for your work.