A Short History of KeY
This paper describes the story of the first nine years of the KeY project, its original goals, the people involved, its setbacks, but also its occasional failures and blind alleys. It is deliberately written in a more personal style, but tries to meet sci
- PDF / 280,547 Bytes
- 16 Pages / 439.37 x 666.142 pts Page_size
- 44 Downloads / 217 Views
Abstract. This paper describes the story of the first nine years of the KeY project, its original goals, the people involved, its setbacks, but also its occasional failures and blind alleys. It is deliberately written in a more personal style, but tries to meet scientific standards of correctness and completeness.
1
The Beginning
The KeY project was conceived on May 14, 1997 in the Abbaye des Pr´emontr´es in Pont-` a-Mousson at the 6th Tableaux Conference. Reiner H¨ ahnle and I and a bottle of red wine retreated in the evening into a quiet and cosy nook of the spectacular conference venue to generate ideas for a NEW project. We were both ready for new challenges. Reiner had just completed his Habilitation. The nationwide focus project on automated deduction (DFG Schwerpunktprogramm “Deduktion”) would come to an end in June 1997 after six successful years. The main results were collected in the monumental book project [13] filling 1250 pages and Wolfgang Bibel published a condensed report [12]. The bulk of research was directed towards theorem proving and theorem provers per se. Applications were seen as the ultimate goal, however, and first steps into applications in mathematics and into software engineering were taken. The examples of applications in software engineering reported in [13] were at very abstract levels. Not a single line of code of an imperative programming language was inspected. That was pretty much the state of the art worldwide. Thus the general direction of follow-up projects was predictable: move deductive support closer to the everyday production of software. But that left open a wide range of choices. Reiner wrote a three-page summary of our brainstorming session the next day (classified, perhaps tongue-in-cheek, “Confidential”). A first rough idea was to develop a methodology and to build a tool for deductive support early on in the specification phase of software systems. The term verification occurred only once in the notes and only in a negative context: We then proposed not to aim for full formal verification but rather for some kind of validation. Considering the lofty goals of the KeY project to come, that was a pussy footed beginning. On the other hand one might view this as a prophetic foresight. In the survey paper [10] on formal verification published 17 years later we find the following sentences: c Springer Nature Switzerland AG 2020 W. Ahrendt et al. (Eds.): Deductive Software Verification, LNCS 12345, pp. 3–18, 2020. https://doi.org/10.1007/978-3-030-64354-6_1
4
P. H. Schmitt
In the past decade, it has become increasingly clear that full functional verification is an elusive goal for almost all application scenarios. Not verification but specification is the real bottleneck in functional verification. The focus of this paper is on the first two KeY project proposals, thus covering the years from 1997 to 2006. Occasionally, when it fits into the story, I will include more recent episodes and events. In general, however, many important later developments of the KeY system are not touched
Data Loading...
