| 1. |
- 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.
|
|
| 2. |
- Beckert, Bernhard, et al.
(författare)
-
The KeY system 1.0 (Deduction Component)
- 2007
-
Ingår i: Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, Springer-Verlag, LNCS. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540735946 ; 4603, s. 379-384
-
Konferensbidrag (refereegranskat)
|
|
| 3. |
- Bubel, R., et al.
(författare)
-
Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic
- 2008
-
Ingår i: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 199, s. 107-128
-
Tidskriftsartikel (refereegranskat)abstract
- The interactive theorem prover developed in the KeY project, which implements a sequent calculus for JavaCard Dynamic Logic (JavaCardDL) is based on taclets. Taclets are lightweight tactics with easy to master syntax and semantics. Adding new taclets to the calculus is quite simple, but poses correctness problems. We present an approach how derived (non-axiomatic) taclets for JavaCardDL can be proven sound in JavaCardDL itself. Together with proof management facilities, our concept allows the safe introduction of new derived taclets while preserving the soundness of the calculus. © 2008 Elsevier B.V. All rights reserved.
|
|
| 4. |
- Engel, Christian, et al.
(författare)
-
Integrating Verification and Testing of Object-Oriented Software
- 2008
-
Ingår i: Tests and Proofs, Second International Conference, TAP 2008, Prato, Italy. Springer, LNCS. - 9783540791232 ; 4966, s. 182-191
-
Konferensbidrag (refereegranskat)abstract
- Formal methods can only gain widespread use in industrial software development if they are integrated into software development techniques, tools, and languages used in practice. A symbiosis of software testing and verification techniques is a highly desired goal, but at the current state of the art most available tools are dedicated to just one of the two tasks: verification or testing. We use the KeY verification system (developed by the tutorial presenters) to demonstrate our approach in combining both.
|
|
| 5. |
- Hähnle, Reiner, 1962, et al.
(författare)
-
Integration of a Security Type System into a Program Logic
- 2007
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Type systems and program logics are often conceived to be at opposing ends of the spectrum of formal software analyses. In this paper we show that a flow-sensitive type system ensuring non-interference in a simple while language can be expressed through specialised rules of a program logic. In our framework, the structure of non-interference proofs resembles the corresponding derivations in a recent security type system, meaning that the algorithmic version of the type system can be used as a proof procedure for the logic. We argue that this is important for obtaining uniform proof certificates in a proof-carrying code framework. We discuss in which cases the interleaving of approximative and precise reasoning allows us to deal with delimited information release. Finally, we present ideas on how our results can be extended to encompass features of realistic programming languages like Java.
|
|
| 6. |
|
|
| 7. |
- Hähnle, Reiner, 1962, et al.
(författare)
-
Integration of a Security Type System into a Program Logic
- 2008
-
Ingår i: Theoretical Computer Science (selected papers from TGC 2006). - : Elsevier BV. - 0304-3975. ; 402:2-3, s. 172-189
-
Tidskriftsartikel (refereegranskat)abstract
- Type systems and program logics are often thought to be at opposing ends of the spectrum of formal software analyses. In this paper we show that a flow-sensitive type system ensuring non-interference in a simple while-language can be expressed through specialised rules of a program logic. In our framework, the structure of non-interference proofs resembles the corresponding derivations in a state-of-the-art security type system, meaning that the algorithmic version of the type system can be used as a proof procedure for the logic. We argue that this is important for obtaining uniform proof certificates in a proof-carrying code framework. We discuss in which cases the interleaving of approximative and precise reasoning allows us to deal with delimited information release. Finally, we present ideas on how our results can be extended to encompass features of realistic programming languages such as Java.
|
|
| 8. |
- Klebanov, Vladimir, et al.
(författare)
-
Verification of JCSP Programs
- 2005
-
Ingår i: Communicating Process Architectures 2005, Concurrent Systems Engineering Series, IOS Press. - 1586035614 ; 63, s. 203-218
-
Konferensbidrag (refereegranskat)abstract
- We describe the first proof system for concurrent programs based on Communicating Sequential Processes for Java (JCSP). The system extends a complete calculus for the JavaCard Dynamic Logic with support for JCSP, which is modeled in terms of the CSP process algebra. Together with a novel efficient calculus for CSP, a rule system is obtained that enables JCSP programs to be executed symbolically and to be checked against temporal properties. The proof system has been implemented within the KeY tool and is publicly available.
|
|
| 9. |
- Rümmer, Philipp, 1978
(författare)
-
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- 2008
-
Ingår i: Logic for Programming, Artificial Intelligence, and Reasoning, Springer, LNCS. - 9783540894384 ; 5330, s. 274-289
-
Konferensbidrag (refereegranskat)abstract
- First-order logic modulo the theory of integer arithmetic is the basis for reasoning in many areas, including deductive software verification and software model checking. While satisfiability checking for ground formulae in this logic is well understood, it is still an open question how the general case of quantified formulae can be handled in an efficient and systematic way. As a possible answer, we introduce a sequent calculus that combines ideas from free-variable constraint tableaux with the Omega quantifier elimination procedure. The calculus is complete for theorems of first-order logic (without functions, but with arbitrary uninterpreted predicates), can decide Presburger arithmetic, and is complete for a substantial fragment of the combination of both.
|
|
| 10. |
- Rümmer, Philipp, 1978
(författare)
-
A Sequent Calculus for Integer Arithmetic with Counterexample Generation
- 2007
-
Ingår i: Proceedings of 4th International Verification Workshop in connection with CADE-21, Bremen, Germany, July 15-16, 2007, CEUR Workshop Proceedings. - 1613-0073. ; 259, s. 179-194
-
Konferensbidrag (refereegranskat)abstract
- We introduce a calculus for handling integer arithmetic in first-order logic. The method is tailored to Java program verification and meant to be used both as a supporting procedure and simplifier during interactive verification and as an automated tool for discharging (ground) proof obligations. There are four main components: a complete procedure for linear equations, a complete procedure for linear inequalities, an incomplete procedure for nonlinear (polynomial) equations, and an incomplete procedure for nonlinear inequalities. The calculus is complete for the generation of counterexamples for invalid ground formula in integer arithmetic. All parts described here have been implemented as part of the KeY verification system.
|
|
