| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(author)
-
The KeY System: Integrating Object-Oriented Design and Formal Methods
- 2002
-
In: 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
-
Conference paper (peer-reviewed)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.
|
|
| 2. |
- Beckert, Bernhard, et al.
(author)
-
Taclets: a new paradigm for writing theorem provers : Taclets: Un nuevo paradigma para construir demostradores automáticos interactivos
- 2004
-
In: REVISTA DE LA REAL ACADEMIA DE CIENCIAS, Serie A: Matemáticas. - 1578-7303. ; 98:1, s. 17-53
-
Journal article (peer-reviewed)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.
|
|
| 3. |
- Beckert, Bernhard, et al.
(author)
-
Taclets: a new paradigm for writing theorem provers
- 2004
-
In: Revista de la Real Academia de Ciencias Exactas, Fisicas y Naturales - Serie A: Matematicas. - 1578-7303 .- 1579-1505. ; 98:1, s. 17-53
-
Journal article (peer-reviewed)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.
|
|
| 4. |
- Beckert, Bernhard, et al.
(author)
-
The KeY system 1.0 (Deduction Component)
- 2007
-
In: 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
-
Conference paper (peer-reviewed)
|
|
| 5. |
- Giese, Martin, 1970
(author)
-
A Calculus for Type Predicates and Type Coercion
- 2005
-
In: utomated Reasoning with Analytic Tableaux and Related Methods, Tableaux 2005, Lecture Notes in Computer Science. ; 3702, s. 123-137
-
Conference paper (peer-reviewed)
|
|
| 6. |
- Giese, Martin, 1970, et al.
(author)
-
From Informal to Formal Specifications in UML
- 2004
-
In: 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. - 3540233075 ; 3273, s. 197-211
-
Journal article (peer-reviewed)abstract
- In this paper, we consider a way of bridging informal and formal specification. Most projects have a need for an informal description of the requirements of the system which all people involved can understand. At the same time, there is a need to make some of the requirements more formal. We present a way to relate informal requirements, in form of use cases, to more formal specifications, written in the Object Constraint Language (OCL). Our approach gives the customers of software systems a way of guiding the development of formal specifications. Conversely, the formal specification can improve the informal understanding of the system by exposing gaps and ambiguities in the informal specification.
|
|
| 7. |
- Giese, Martin, 1970, et al.
(author)
-
Rule-Based Simplification of OCL Constraints
- 2004
-
In: OCL and Model Driven Engineering, UML 2004 workshop, Lisbon. ; , s. 84-98
-
Conference paper (peer-reviewed)abstract
- To help designers in writing OCL constraints, we have to construct systems that can generate some of these constraints. This might be done by instantiating templates, by combining prefabricated parts, or by more general computation. Such generated specifications will often contain redundancies that reduce their readability. In this paper, we explore the possibilities of simplifying OCL formulae through the repeated application of simple rules. We discuss the different kinds of rules that are needed, and we describe a prototypical implementation of the approach.
|
|
| 8. |
- Giese, Martin, 1970
(author)
-
Simplification Rules for Constrained Formula Tableaux
- 2003
-
In: 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. - 3540407871 ; 2796, s. 65-80
-
Conference paper (peer-reviewed)abstract
- Several vaxiants of a first-order simplification rule for non-normal form tableaux using syntactic constraints axe presented. These can be used as a framework for porting methods like unit resolution or hyper tableaux to non-normal form free variable tableaux.
|
|
| 9. |
- Giese, Martin, 1970
(author)
-
Taclets and the KeY Prover
- 2004
-
In: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 103, s. 67-79
-
Journal article (peer-reviewed)abstract
- We give a short overview of the KeY prover---which is the proof system belonging to the KeY tool---from a user interface perspective. In particular, we explain the concept of taclets, which are the basic building blocks for proofs in the KeY prover.
|
|
| 10. |
- Hähnle, Reiner, 1962, et al.
(author)
-
The KeY Tool
- 2005
-
In: Software and Systems Modeling. - 1619-1374 .- 1619-1366. ; 4:1, s. 32-54
-
Journal article (peer-reviewed)
|
|
