| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Deductive Software Verification - The KeY Book
- 2016
-
Bok (övrigt vetenskapligt/konstnärligt)abstract
- Static analysis of software with deductive methods is a highly dynamic field of research on the verge of becoming a mainstream technology in software engineering. It consists of a large portfolio of - mostly fully automated - analyses: formal verification, test generation, security analysis, visualization, and debugging. All of them are realized in the state-of-art deductive verification framework KeY. This book is the definitive guide to KeY that lets you explore the full potential of deductive software verification in practice. It contains the complete theory behind KeY for active researchers who want to understand it in depth or use it in their own work. But the book also features fully self-contained chapters on the Java Modeling Language and on Using KeY that require nothing else than familiarity with Java. All other chapters are accessible for graduate students (M.Sc. level and beyond). The KeY framework is free and open software, downloadable from the book companion website which contains also all code examples mentioned in this book.
|
|
| 2. |
|
|
| 3. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
KeY: A Formal Method for Object-Oriented Systems
- 2007
-
Ingår i: Lecture Notes in Computer Science, Proc. 9th IFIP Intl. Conf. on Formal Methods for Open Object-based Distributed Systems (FMOODS), eds. M.Bonsangue and E. B. Johnsen. ; 4468, s. 32-43
-
Konferensbidrag (refereegranskat)
|
|
| 4. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
The KeY platform for verification and analysis of java programs
- 2014
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 8471:8471, s. 55-71
-
Konferensbidrag (refereegranskat)abstract
- The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flowsecurity, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.
|
|
| 5. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
The KeY System: Integrating Object-Oriented Design and Formal Methods
- 2002
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783540433538 ; 2306, s. 327-330
-
Konferensbidrag (refereegranskat)abstract
- This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project1, which is aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. The KeY system consists of a commercial CASE tool enhanced with functionality for formal specification and deductive verification.
|
|
| 6. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Verifying Object-Oriented Programs with KeY: A Tutorial
- 2007
-
Ingår i: Formal Methods for Components and Objects, eds. de Boer, Bonsangue, Graf, de Roever. - 9783540747918 ; LNCS 4709
-
Konferensbidrag (refereegranskat)abstract
- This paper is a tutorial on performing formal specification and semi-automatic verification of Java programs with the formal software development tool KeY. This tutorial aims to fill the gap between elementary introductions using toy examples and state-of-art case studies by going through a self-contained, yet non-trivial, example. It is hoped that this contributes to explain the problems encountered in verification of imperative, object-oriented programs to a readership outside the limited community of active researchers.
|
|
| 7. |
- Albert, Elvira, et al.
(författare)
-
Verified resource guarantees for heap manipulating programs
- 2012
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642288715 ; 7212, s. 130-145
-
Konferensbidrag (refereegranskat)abstract
- Program properties that are automatically inferred by static analysis tools are generally not considered to be completely trustworthy, unless the tool implementation or the results are formally verified. Here we focus on the formal verification of resource guarantees inferred by automatic cost analysis. Resource guarantees ensure that programs run within the indicated amount of resources which may refer to memory consumption, to number of instructions executed, etc. In previous work we studied formal verification of inferred resource guarantees that depend only on integer data. In realistic programs, however, resource consumption is often bounded by the size of heap-allocated data structures. Bounding their size requires to perform a number of structural heap analyses. The contributions of this paper are (i) to identify what exactly needs to be verified to guarantee sound analysis of heap manipulating programs, (ii) to provide a suitable extension of the program logic used for verification to handle structural heap properties in the context of resource guarantees, and (iii) to improve the underlying theorem prover so that proof obligations can be automatically discharged.
|
|
| 8. |
- Albert, Elvira, et al.
(författare)
-
Verified Resource Guarantees using COSTA and KeY
- 2011
-
Ingår i: Proc. ACM SIGPLAN 2011 Workshop on Partial Evaluation and Program Manipulation (PEPM'11), ACM Press. - New York, NY, USA : ACM. - 9781450304856 ; , s. 73-76
-
Konferensbidrag (refereegranskat)abstract
- Resource guarantees allow being certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. This information can be very useful, especially in real-time and safety-critical applications. Nowadays, a number of automatic tools exist, often based on type systems or static analysis, which produce such resource guarantees. In spite of being based on theoretically sound techniques, the implemented tools may contain bugs which render the resource guarantees thus obtained not completely trustworthy. Performing full-blown verification of such tools is a daunting task, since they are large and complex. In this work we investigate an alternative approach whereby, instead of the tools, we formally verify the results of the tools. We have implemented this idea using COSTA, a state-of-the-art static analysis system, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Our preliminary results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.
|
|
| 9. |
|
|
| 10. |
- Beckert, Bernhard, et al.
(författare)
-
Taclets: a new paradigm for writing theorem provers : Taclets: Un nuevo paradigma para construir demostradores automáticos interactivos
- 2004
-
Ingår i: REVISTA DE LA REAL ACADEMIA DE CIENCIAS, Serie A: Matemáticas. - 1578-7303. ; 98:1, s. 17-53
-
Tidskriftsartikel (refereegranskat)abstract
- Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules of calculi have not only purely logical content, but contain restrictions on the expected context of rule applications and heuristic information. We suggest a new and minimalist concept for implementing interactive theorem provers called taclet. Their usage can be mastered in a matter of hours, and they are efficiently compiled into the GUI of a prover. We implemented the KeY system, an interactive theorem prover for the full JavaCard language based on taclets.
|
|
