– Discussion Paper – Must Program Verification Systems and Calculi Be Verified? (2008)
Bernhard Beckert, Vladimir Klebanov
Abstract. With this paper, we want to provoke discussion on whether verification tools and calculi themselves need to be formally verified. We argue that though verifying the verifier is useful, it...
Bernhard Beckert, Joachim Posegga
Researchers in Automated Reasoning often complain that there are sparse applications of the techniques they
Bernhard Beckert, Joachim Posegga
> The idea of lean deduction is to achieve maximal efficiency from minimal means. Every possible effort is made to eliminate overhead. Logic programming languages provide an ideal tool for...
Free-variable tableaux for propositional modal logics (2008)
Abstract. Free-variable semantic tableaux are a well-established technique for first-order theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used...
Second-Order Principles in Specification Languages for Object-Oriented Programs (2008)
Bernhard Beckert, Kerry Trentelman
Abstract. Within the setting of object-oriented program specification and verification, pointers and object references can be considered as relations between the elements of a data structure. When we...
Guaranteeing Consistency in Text-Based Human-Computer-Interaction (2008)
Bernhard Beckert, Gerd Beuster
Wrong assumptions about the state of the computer system are a main source of error in human-computer interaction. We show how consistency requirements between the state of a computer system and the...
Bernhard Beckert, Steffen Schlager
Abstract. Refinement is a well-established and accepted technique for the systematic development of correct software systems. However, for the step from already refined specification to...
Rev R. Acad, Cien Serie, A. Mat, Bernhard Beckert, Martin Giese, Elmar Habermalz, ...
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...
Verifying Object-Oriented Programs with KeY: A Tutorial (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
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...
Verifying Object-Oriented Programs with KeY: A Tutorial (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
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...
KeY: A Formal Method for Object-Oriented Systems (2008)
Wolfgang Ahrendt, Bernhard Beckert, Peterh. Schmitt
Abstract. This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of object-oriented...
Taclets: A New Paradigm for Constructing Interactive Theorem Provers (2008)
Rev R. Acad, Cien Serie, A. Mat, Bernhard Beckert, Martin Giese, Elmar Habermalz, ...
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...
KeY: A Formal Method for Object-Oriented Systems (2008)
Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. This paper gives an overview of the KeY approach and highlights the main features of the KeY system. KeY is an approach (and a system) for the deductive verification of object-oriented...
Bernhard Beckert, Steffen Schlager
Abstract. Refinement is a well-established and accepted technique for the systematic development of correct software systems. However, for the step from already refined specification to...
was the 14th in a series of international meetings since 1992 (listed on the
Content-Length: 59824 Status: RO On Anti-Links † (2008)
Bernhard Beckert, Reiner H, Anavai Ramesh, Neil V. Murray
Abstract. The concept of anti-link is defined, and useful equivalence-preserving operations on propositional formulas based on anti-links are introduced. These operations eliminate a potentially...
Bernhard Beckert, Reiner Hähnle, Neil V. Murray, Anavai Ramesh
Manipulation of Boolean functions has important applications in such fields as hardware verification, non-monotonic reasoning, and decision support. Most often, in such applications, the set of prime...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
Abstract KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal...
Reusing Proofs when Program Verification Systems are Modified (2008)
Bernhard Beckert, Thorsten Bormer, Vladimir Klebanov
In this position paper, we describe ongoing work on reusing deductive proofs for program correctness when the verification system itself is modified (including its logic, its calculus, and its proof...
Guaranteeing Consistency in Text-Based Human-Computer-Interaction (2008)
Bernhard Beckert, Gerd Beuster
Wrong assumptions about the state of the computer system are a main source of error in human-computer interaction. We show how consistency requirements between the state of a computer system and the...
Chapter 1 THE SAT PROBLEM OF SIGNED CNF FORMULAS (2008)
Bernhard Beckert, Reiner Hähnle, Felip Manyà
Abstract Signed conjunctive normal form (signed CNF) is a classical conjunctive clause form using a generalised notion of literal, called signed literal. A signed literal is an expression of the form...
Propositional Non Clausal Deduction and Diagnosis (2008)
Anavai Ramesh, Neil V. Murray, Bernhard Beckert, Reiner Hähnle
In [11] Reiter laid the foundations of the formal theory of an approach to diagnosis known as diagnosis from first principles. His work was based on the work of many researchers, notably that of de...
Formal Specification of Security-relevant Properties of User Interfaces 1 (Extended Version) (2008)
Bernhard Beckert, Gerd Beuster
Abstract. When sensitive information is exchanged with the user of a computer system, the security of the system’s user interface must be considered. In this paper, we show how security relevant...
CHAPTER 1 EQUALITY AND OTHER THEORIES (2008)
Theory reasoning is an important technique for increasing the efficiency of automated deduction systems. The knowledge from a given domain (or theory) is made use of by applying efficient methods for...
Bernhard Beckert, Vladimir Klebanov, Steffen Schlager
In the previous chapter, we have introduced a variant of classical predicate logic that has a rich type system and a sequent calculus for that logic. This predicate logic can easily be used to...
Proving Compiler Correctness with Evolving Algebra (2008)
Speci Cations, Bernhard Beckert, Reiner Hahnle
The purpose of this note is to de ne a framework for proving compiler correctness with evolving algebra (EA) speci cations [2]. Although our speci c domain is the veri cation of a Prolog-to-
The Even More Liberalized δ-Rule in Free Variable Semantic Tableaux (2008)
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
. In this paper we have a closer look at one of the rules of the tableau calculus presented in [3], called the ffi--rule, and the modification of this rule, that has been proved to be sound and...
This volume contains those research papers presented at the Second International Conference on Tests and Proofs (TAP 2008) that were not included in the main conference proceedings1. TAP was the...
Workshop Program 5th International Verification Workshop – VERIFY’08 (2008)
Bernhard Beckert, Gerwin Klein (chairs, Bernhard Beckert, Bernhard Beckert, Gerwin Klein, ...
The VERIFY workshop series aims at bringing together people who are interested in the development of safety and security critical systems, in formal methods, in the development of automated theorem...
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz
2, Wolfram Menzel 1, and Peter H. Schmitt 1 1
The Tableau-based Theorem Prover (2007)
Version Bernhard Beckert, Bernhard Beckert, Reiner Hahnle, Peter Oel, Martin Sulzmann
This paper gives an overview of the system with a special focus on the new features of 3 T A P Version 4.0, including: efficient completion-based equality reasoning, methods for handling redundant...
Bernhard Beckert, Reiner Hahnle, Gonzalo Escalada-imaz
We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of antilinks....
Wolfgang Ahrendt, Bernhard Beckert, Wolfram Menzel
Reif 2, Gerhard Schellhorn 2 and Peter Schmitt 1 1
Using Mixed Universal and Rigid (2007)
Unification To Handle, Bernhard Beckert
Bernhard Beckert University of Karlsruhe Institute for Logic, Complexity und Deduction Systems 76128 Karlsruhe, Germany beckert@ira.uka.de Abstract. In this paper we describe how a combination of the...
The Approach: Integrating Object Oriented Design and Formal Veri cation (2007)
Wolfgang Ahrendt Thomas, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel, ...
. This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verication. A distinctive feature of our approach is...
Integer Arithmetic in the Specication and Verication of Java Programs (2007)
Abstract. In this paper we present an approach for handling integer arithmetic in the specication and verication of Java programs. In particular, problems like over ow and under ow arising from the...
FASE System Description The System: Integrating Object-Oriented Design and Formal Methods ⋆ (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
Abstract. This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1, which is aimed at bridging the gap between (a) OO software engineering methods...
Depth- rst Proof Search without Backtracking for Free-variable (2007)
Clausal Tableaux, Bernhard Beckert
Abstract. We analyse the problem of constructing a deterministic proof procedure for free-variable clausal tableaux that performs depth-rst proof search without backtracking; and we present a...
Content-Length: 59824 Status: RO On Anti-Links † (2007)
Bernhard Beckert, Reiner H, Anavai Ramesh, Neil V. Murray
Abstract. The concept of anti-link is defined, and useful equivalence-preserving operations on propositional formulas based on anti-links are introduced. These operations eliminate a potentially...
Deduction by Combining Semantic Tableaux and Integer Programming (2007)
Bernhard Beckert, Reiner Hahnle
Abstract. In this paper we propose to extend the current capabilities of automated reasoning systems by making use of techniques from integer programming. We describe the architecture of an automated...
Deduction by Combining Semantic Tableaux and Integer Programming (2007)
Bernhard Beckert, Reiner Hahnle
Abstract. In this paper we propose to extend the current capabilities of automated reasoning systems by making use of techniques from integer programming. We describe the architecture of an automated...
Institute for Logic, Complexity, and Deduction Systems (2007)
Bernhard Beckert, Reiner Hahnle, Neil V. Murray, Anavai Ramesh
Manipulation of Boolean functions has important applications in such fields as hardware verification, non-monotonic reasoning, and decision support. Most often, in such applications, the set of prime...
Extending Hyper Tableaux with Rigid E-Unification (2007)
Peter Baumgartner, Michael Kuhn, Bernhard Beckert
In [BFN96] we introduced a variant of clausal normal form tableaux called "hyper tableaux". Hyper tableaux keep many desirable features of analytic tableaux (structure of proofs,...
Bernhard Beckert, Joachim Posegga
Researchers in Automated Reasoning often complain that there are sparse applications of the techniques they develop. One reason might be that implementation-oriented research favors huge and highly...
Thomas Baar, Bernhard Beckert, Peter H. Schmitt
Abstract. We consider rst-order Dynamic Logic (DL) with non-rigid functions, which can be used to model certain features of programming languages such as array variables and object attributes. We...
PMD '01 Precise Modelling and Deduction for Object-oriented Software Development (2007)
Bernhard Beckert, Bart Jacobs, Johann Schumann, Jon Whittle
(eds.)
Bernhard Beckert, Reiner Hahnle, Gonzalo Escalada-imaz
Abstract. We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of...
Bernhard Beckert, Reiner Hahnle, Peter Oel, Martin Sulzmann
3 T A P is a tableau-based theorem prover for many-valued first-order logics with sorts (in the two-valued version with equality); it is implemented in Prolog. This paper gives an overview of the...
A Dynamic Logic for the Formal Verication of Java Card Programs (2007)
i12www.ira.uka.de/~beckert Abstract. In this paper, we dene a program logic (an instance of Dynamic Logic) for formalising properties of Java Card programs, and we give a sequent calculus for...
Abstract. In this paper we describe how a combination of the classical "universal " E-unification and "rigid " E-unification, called "mixed "...
Institute for Logic, Complexity, and Deduction Systems (2007)
Anavai Ramesh, Neil V. Murray, Bernhard Beckert, Reiner Hahnle
In [11] Reiter laid the foundations of the formal theory of an approach to diagnosis known as diagnosis from first principles. His work was based on the work of many researchers, notably that of de...
We analyse the problem of constructing a deterministic proof procedure for free-variable clausal tableaux that performs depth-rst proof search without backtracking; and we present a solution based on...
Anavai Ramesh, Bernhard Beckert, Reiner Hahnle, Neil V. Murray
Abstract. The concept of anti-link is defined (an anti-link consists of two occurrences of the same literal in a formula), and useful equivalence-preserving operations based on anti-links are...
Researchers in Automated Reasoning often com- 1 prove((A,B),UnExp,Lits,FreeV,VLim):-!, (2007)
Bernhard Beckert, Joachim Posegga
2 prove((A;B),UnExp,Lits,FreeV,VLim):-!, prove(A,UnExp,Lits,FreeV,VLim), prove(B,UnExp,Lits,FreeV,VLim). 3 prove(all(X,Fml),UnExp,Lits,FreeV,VLim):-!, \+ length(FreeV,VLim),...
Bernhard Beckert, Wojciech Mostowski
Abstract. In this paper we extend a program logic for verifying JAVA CARD applications by introducing a \throughout " operator that allows us to prove \strong " invariants. Strong...
Depth- rst Proof Search without Backtracking (2007)
We analyse the problem of constructing a deterministic proof procedure for free-variable clausal tableaux that performs depth-rst proof search without backtracking; and we present a solution based on...
Formal Specification of Security-relevant Properties of User Interfaces 1 (2007)
Bernhard Beckert, Gerd Beuster
Abstract. When sensitive information is exchanged with the user of a computer system, the security of the system’s user interface must be considered. In this paper, we show how security relevant...
Technical Report no. 2003-05 The KeY Tool 1 (2007)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
Formal Specification of Security-relevant Properties of User Interfaces ∗ (2007)
Bernhard Beckert, Bernhard Beckert, Gerd Beuster, Gerd Beuster
When sensitive information is exchanged with the user of a computer system, the security of the system’s user interface must be considered. In this paper, we show how security relevant properties...
Bernhard Beckert, Ste#en Schlager
Abstract. We present an approach to integrating the refinement relation between infinite integer types (used in specification languages) and finite integer types (used in programming languages) into...
Taclets: A New Paradigm for Constructing Interactive Theorem Provers (2007)
Rev R. Acad, Cien Serie, A. Mat, Bernhard Beckert, Martin Giese, Elmar Habermalz, ...
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...
Simplification of many-valued logic formulas using anti-links. (2007)
Beckert, Bernhard, Haehnle, Reiner, Escalada-Imaz, Gonzalo
We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called "removal of anti-links"....
Incremental theory reasoning methods for semantic tableaux. (2007)
Beckert, Bernhard, Pape, Christian
Theory reasoning is an important technique for increasing the efficiency of automated deduction systems. In this paper we present incremental theory reasoning, a method that improves the interaction...
Proving compiler correctness with evolving algebra specifications. (2007)
Beckert, Bernhard, Haehnle, Reiner
The purpose of this note is to define a framework for proving compiler correctness with evolving algebra (EA) specifications. Although our specific domain is the verification of a Prolog-to-WAM...
Fast subsumption checks using anti-links. (2007)
Ramesh, Anavai, Murray, Neil V., Beckert, Bernhard, Haehnle, Reiner
The concept of "anti-link" is defined, and useful equivalence-preserving operations based on anti-links are introduced.These operations eliminate a potentially large number of subsumed paths in a...
The many-valued theorem prover 3TAP. 3rd. edition. (2007)
Hähnle, Reiner, Beckert, Bernhard, Gerberding, Stefan
This is the 3TAP handbook. 3TAP is a many-valued tableau-based theorem prover developed at the University of Karlsruhe. The handbook serves a triple purpose: first, it documents the history and...
leanEA. A poor man's evolving algebra compiler. (2007)
Beckert, Bernhard, Posegga, Joachim
The Prolog program term_expansion((define C as A with B), (C=>A:-B,!)). term_expansion((transition E if C then D), ((transition E):-C,!,B,A,(transition _))) :- serialize(D,B,A)....
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
White-box testing by combining deduction-based specification extraction and black-box testing (2007)
Bernhard Beckert, Christoph Gladisch
Abstract. We propose to use deductive program verification systems to generate specifications for given programs and to then use these specifications as input for black-box testing tools. In this...
The KeY System 1.0 (deduction component (2007)
Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Steffen Schlager, Peter H. Schmitt
www.key-project.org Abstract. The KeY system is a development of the ongoing KeY project, whose aim is to integrate formal specification and deductive verification into the industrial software...
Bernhard Beckert, Yves Bertot, Inria Sophia Antipolis
The VERIFY workshop series aims at bringing together people who are interested in the development of safety and security critical systems, in formal methods, in the development of automated theorem...
A method for formalizing, analyzing, and verifying secure user interfaces (2006)
Bernhard Beckert, Gerd Beuster
Abstract. We present a methodology for the formalization of humancomputer interaction under security aspects. As part of the methodology, we give formal semantics for the well-known GOMS methodology...
Dynamic logic with non-rigid functions: A basis for object-oriented program verification (2006)
Bernhard Beckert, André Platzer
Abstract. We introduce a dynamic logic that is enriched by non-rigid functions, i.e., functions that may change their value from state to state (during program execution), and we present a...
A method for formalizing, analyzing, and verifying secure user interfaces (2006)
Bernhard Beckert, Gerd Beuster
Abstract. We present a methodology for the formalization of humancomputer interaction under security aspects. As part of the methodology, we give formal semantics for the well-known GOMS methodology...
Dynamic logic with non-rigid functions: A basis for object-oriented program verification (2006)
Bernhard Beckert, André Platzer
Abstract. We introduce a dynamic logic that is enriched by non-rigid functions, i.e., functions that may change their value from state to state (during program execution), and we present a...
An improved rule for while loops in deductive program verification (2005)
Beckert, Bernhard, Schlager, Steffen, Schmitt, Peter H.
The performance and usability of deductive program verification systems can be greatly enhanced if specifications of programs and program parts not only consist of the usual pre-/post-condition pairs...
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Bubel, Richard, Giese, Martin, Hähnle, Reiner, ...
KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and...
An improved rule for while loops in deductive program verification (2005)
Bernhard Beckert, Steffen Schlager, Peter H. Schmitt
Abstract. The performance and usability of deductive program verification systems can be greatly enhanced if specifications of programs and program parts not only consist of the usual...
Description Logics for Shape Analysis (2005)
Georgieva, Lilia, Maier, Patrick, Aichernig, Bernhard K., Beckert, Bernhard
Verification of programs requires reasoning about sets of program states. In case of programs manipulating pointers, program states are pointer graphs. Verification of such programs involves...
Verification of an Off-Line Checker for Priority Queues (2005)
De Nivelle, Hans, Piskac, Ruzica, Aichernig, Bernhard K., Beckert, Bernhard
Comparing Instance Generation Methods for Automated Reasoning (2005)
Jacobs, Swen, Waldmann, Uwe, Beckert, Bernhard
The clause linking technique of Lee and Plaisted proves the unsatisfiability of a set of first-order clauses by generating a sufficiently large set of instances of these clauses that can be shown to...
Taclets: A New Paradigm for Constructing Interactive Theorem Provers (2004)
Bernhard Beckert, Bernhard Beckert, Martin Giese, Martin Giese, Elmar Habermalz, Reiner Hähnle, ...
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...
In Formal Methods for Open Object-Based Distributed Systems (2004)
Abb Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, ...
[AdB90] Pierre America and Frank de Boer. Proving total correctness of recursive procedures. Information and Computation, 84(2):129– 162, 1990. [AdB94] Pierre America and Frank de Boer. Reasoning...
Software verification with integrated data type refinement for integer arithmetic (2004)
Bernhard Beckert, Steffen Schlager
Abstract. We present an approach to integrating the refinement relation between infinite integer types (used in specification languages) and finite integer types (used in programming languages) into...
Software verification with integrated data type refinement for integer arithmetic (2004)
Bernhard Beckert, Steffen Schlager
Abstract. We present an approach to integrating the refinement relation between infinite integer types (used in specification languages) and finite integer types (used in programming languages) into...
A program logic for handling Java Card’s transaction mechanism (2003)
Bernhard Beckert, Wojciech Mostowski
Abstract. In this paper we extend a program logic for verifying JAVA CARD applications by introducing a “throughout ” operator that allows us to prove “strong ” invariants. Strong invariants...
A program logic for handling Java Card’s transaction mechanism (2003)
Bernhard Beckert, Wojciech Mostowski
Abstract. In this paper we extend a program logic for verifying JAVA CARD applications by introducing a “throughout ” operator that allows us to prove “strong ” invariants. Strong invariants...
Program verification using change information (2003)
Bernhard Beckert, Peter H. Schmitt
i12www.ira.uka.de/key We propose an extension of the design-by-contract approach. In addition to preconditions, postconditions, and invariants as the basis for proving properties of a program, also...
Program verification using change information (2003)
Bernhard Beckert, Peter H. Schmitt
i12www.ira.uka.de/˜key We propose an extension of the design-by-contract approach. In addition to preconditions, postconditions, and invariants as the basis for proving properties of a program, also...
The KeY system: Integrating object-oriented design and formal methods (2002)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Elmar Habermalz, Wolfram Menzel, Wojciech Mostowski, ...
Abstract. This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1, which is aimed at bridging the gap between (a) OO software engineering methods...
Translating the Object Constraint Language into First-order Predicate Logic (2002)
Bernhard Beckert, Uwe Keller, Peter H. Schmitt
Abstract. In this paper, we define a translation of UML class diagrams with OCL constraints into first-order predicate logic. The goal is logical reasoning about UML models, realized by an...
Translating the Object Constraint Language into First-order Predicate Logic (2002)
Bernhard Beckert, Uwe Keller, Peter H. Schmitt
Abstract. In this paper, we define a translation of UML class diagrams with OCL constraints into first-order predicate logic. The goal is logical reasoning about UML models. We put an emphasis on...
Translating the Object Constraint Language into First-order Predicate Logic (2002)
Bernhard Beckert, Uwe Keller, Peter H. Schmitt
Abstract. In this paper, we define a translation of UML class diagrams with OCL constraints into first-order predicate logic. The goal is logical reasoning about UML models, realized by an...
Handling JAVA’s abrupt termination in a sequent calculus for Dynamic Logic (2001)
Bernhard Beckert, Bettina Sasse
Abstract. In Java, the execution of a statement can terminate abruptly (besides terminating normally and terminating not at all). Abrupt termination either leads to a redirection of the control ow...
A sequent calculus for first-order dynamic logic with trace modalities (2001)
Abstract. The modalities of Dynamic Logic refer to the nal state of a program execution and allow to specify programs with pre- and postconditions. In this paper, we extend Dynamic Logic with...
An Extension of Dynamic Logic (2001)
For Modelling Ocl's, Thomas Baar, Bernhard Beckert, Peter H. Schmitt
We consider rst-order Dynamic Logic (DL) with non-rigid functions, which can be used to model certain features of programming languages such as array variables and object attributes. We extend this...
The KeY approach: integrating object oriented design and formal verification. (2000)
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Haehnle, Reiner, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
The KeY approach: integrating object oriented design and formal verification. (2000)
Ahrendt, Wolfgang, Baar, Thomas, Beckert, Bernhard, Giese, Martin, Habermalz, Elmar, Haehnle, Reiner, ...
A Dynamic Logic for Java Card (2000)
i12www.ira.uka.de/~beckert Abstract. In this paper, I describe a Dynamic Logic for Java Card and outline a sequent calculus for this logic that axiomatises Java Card. The purpose of the logic is to...
A Dynamic Logic for Java Card (2000)
i12www.ira.uka.de/~beckert Abstract. In this paper, I describe a Dynamic Logic for Java Card and outline a sequent calculus for this logic that axiomatises Java Card. The purpose of the logic is to...
Depth-first proof search without backtracking for free variable semantic tableaux (2000)
We analyse the problem of constructing a deterministic proof procedure for free variable clausal tableaux that performs depth-first proof search without backtracking; and we present a solution based...
The 2-SAT problem of regular signed CNF formulas (2000)
Bernhard Beckert, Reiner Hahnle, Felip Manya
Signed conjunctive normal form (signed CNF) is a classical conjunctive clause form using a generalized notion of literal, called signed atom. A signed atom is an expression of the form S: p, where p...
The KEY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, ...
This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is...
Depth-first proof search without backtracking for free variable semantic tableaux (2000)
We analyse the problem of constructing a deterministic proof procedure for free variable clausal tableaux that performs depth-first proof search without backtracking; and we present a solution based...
The KeY Approach: Integrating Object Oriented Design and Formal Verification (2000)
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Wolfram Menzel, ...
Abstract This paper reports on the ongoing KeY project aimed at bridging the gap between (a) object-oriented software engineering methods and tools and (b) deductive verification. A distinctive...
The 2-SAT problem of regular signed CNF formulas (2000)
Signed conjunctive normal form (signed CNF) is a classical conjunctive clause form using a generalized notion of literal, called signed atom. A signed atom is an expression of the formË�Ô,...
Proof transformations from search-oriented into interaction-oriented tableau calculi (1999)
Gernot Stenz, Wolfgang Ahrendt, Bernhard Beckert
Abstract: Logic calculi, and Gentzen-type calculi in particular, can be categorised into two types: search-oriented and interaction-oriented calculi. Both these types have certain...
Transformations between signed and classical clause logic (1999)
Bernhard Beckert, Reiner Hahnle
Abstract. In the last years two automated reasoning techniques for clause normal form arose in which the use of labels are prominently featured: signed logic and annotated logic programming, which...
Transformations between Signed and Classical Clause Logic (1999)
Bernhard Beckert, Reiner Hähnle, Felip Manyà
In the last years two automated reasoning techniques for clause normal form arose in which the use of labels are prominently featured: signed logic and annotated logic programming, which can be...
Transformations between signed and classical clause logic (1999)
Bernhard Beckert, Reiner Hähnle
In the last years two automated reasoning techniques for clause normal form arose in which the use of labels are prominently featured: signed logic and annotated logic programming, which can be...
Integration und Uniformierung von Methoden des tableaubasierten Theorembeweisens / (1998)
Karlsruhe, Universiẗat, Diss., 1998 (Nicht für den Austausch).
Fibring semantic tableaux (1998)
Abstract. The methodology of fibring is a successful framework for combining logical systems based on combining their semantics. In this paper, we extend the fibring approach to calculi for logical...
System description: leanK 2.0 (1998)
Abstract. leanK is a “lean”, i.e., extremely compact, Prolog implementation of a free variable tableau calculus for propositional modal logics. leanK 2.0 includes additional search space...
By replacing syntactical unification with rigid E-unification, equality handling can be added to rigid variable calculi for first-order logic, including
System description: leanK 2.0 (1998)
Abstract. leanK is a “lean”, i.e., extremely compact, Prolog implementation of a free variable tableau calculus for propositional modal logics. leanK 2.0 includes additional search space...
By replacing syntactical unification with rigid E-unification, equality handling can be added to rigid variable calculi for first-order logic, including
Integrating automated and interactive theorem proving (1998)
Wolfgang Ahrendt, Bernhard Beckert, Wolfram Menzel, Wolfgang Reif, Gerhard Schellhorn, Peter Schmitt
Abstract. This paper highlights a project to integrate interactive and automated theorem proving in Software Verification. Its aim is to combine the advantages of the two paradigms. We report on the...
A tableau calculus for quantifier-free set theoretic formulae (1998)
Bernhard Beckert, Ulrike Hartmer
Abstract. Set theory is the common language of mathematics. Therefore, set theory plays an important rôle in many important applications of automated deduction. In this paper, we present an improved...
Simplification of Many-Valued Logic Formulas Using Anti-Links (1998)
BECKERT, BERNHARD, HÄHNLE, REINER, ESCALADA-IMAZ, GONZALO
The theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, called removal of anti-links are presented. Possible...
Fast subsumption checks using anti-links (1997)
Interner Bericht, Fakultat Fur Informatik, Anavai Ramesh, Anavai Ramesh, Neil V. Murray, Neil V. Murray, ...
This report has been submitted for publication elsewhere, and will be copyrighted if accepted.
Free variable tableaux for propositional modal logics (1997)
Interner Bericht, Fakultat Fur Informatik, Bernhard Beckert, Bernhard Beckert
We present a sound, complete, modular and lean labelled tableau calculus for many propositional modal logics where the labels contain "free" and "universal "...
Bernhard Beckert, Reiner Hahnle
Abstract. We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of...
Free Variable Tableaux for Propositional Modal Logics (1997)
. We present a sound, complete, modular and lean labelled tableau calculus for many propositional modal logics where the labels contain "free" and "universal" variables. Our...
Simplification of Many-Valued Formulas . . . (1997)
Bernhard Beckert, Reiner Hähnle, Gonzalo Escalada-Imaz
We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of anti-links....
Simplification of Many-Valued Logic Formulas Using Anti-Links (1997)
Bernhard Beckert, Reiner Hähnle, Gonzalo Escalada-imaz
We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of antilinks....
Free Variable Tableaux for Propositional Modal Logics (1997)
We present a sound, complete, modular and lean labelled tableau calculus for many propositional modal logics where the labels contain "free" and "universal" variables. Our...
Free variable tableaux for propositional modal logics (1997)
Abstract. We present a sound, complete, modular and lean labelled tableau calculus for many propositional modal logics where the labels contain “free ” and “universal ” variables. Our “lean...
Free-variable Tableaux for Propositional Modal Logics (1997)
Free-variable semantic tableaux are a well-established technique for first-order theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof...
Semantic Tableaux with Equality (1997)
This paper tries to identify the basic problems encountered in handling equality in the semantic tableau framework, and to describe the state of the art in solving these problems. The two main...
The tableau-based theorem prover 3TAP. Version 4.0 (1996)
Beckert, Bernhard, Haehnle, Reiner, Oel, Peter, Sulzmann, Martin
The tableau-based theorem prover 3TAP. Version 4.0. (1996)
Beckert, Bernhard, Haehnle, Reiner, Oel, Peter, Sulzmann, Martin
Incremental theory reasoning methods for semantic tableaux (1996)
Bernhard Beckert, Christian Pape
Abstract. Theory reasoning is an important technique for increasing the efficiency of automated deduction systems. In this paper we present incremental theory reasoning, a method that improves the...
leanEA: A lean evolving algebra compiler (1996)
Bernhard Beckert, Joachim Posegga
"termexpansion((define C as A with B), (C=?A:-B,!)). termexpansion((transition E if C then D), ((transition E):-C,!,B,A,(transition))):-serialize(D,B,A). serialize((E,F),(C,D),(A,B)):-...
leanEA: A lean evolving algebra compiler (1996)
Bernhard Beckert, Joachim Posegga
"termexpansion((define C as A with B), (C=?A:-B,!)). termexpansion((transition E if C then D), ((transition E):-C,!,B,A,(transition))):-serialize(D,B,A). serialize((E,F),(C,D),(A,B)):-...
Incremental theory reasoning methods for semantic tableaux (1996)
Bernhard Beckert, Christian Pape
Abstract. Theory reasoning is an important technique for increasing the efficiency of automated deduction systems. In this paper we present incremental theory reasoning, a method that improves the...
Proving Compiler Correctness with Evolving Algebra Specifications (1996)
Bernhard Beckert, Reiner Hähnle
Introduction The purpose of this note is to define a framework for proving compiler correctness with evolving algebra (EA) specifications [2]. Although our specific domain is the verification of a...
Fakultat Fur, Interner Bericht, Fakultat Fur Informatik, Bernhard Beckert, Bernhard Beckert
We present a sound, complete, modular and lean labelled tableau calculus for many propositional modal logics where the labels contain "free" and "universal" variables. Our...
leanEA: A lean evolving algebra compiler (1996)
Bernhard Beckert, Joachim Posegga
Abstract. The Prolog program “term_expansion((define C as A with B), (C=>A:-B,!)). term_expansion((transition E if C then D), ((transition E):-C,!,B,A,(transition _))):serialize(D,B,A)....
Fast subsumption checks using anti-links. (1995)
Ramesh, Anavai, Murray, Neil V., Beckert, Bernhard, Haehnle, Reiner
leanEA: A Poor Man's Evolving Algebra Compiler, research report (1995)
Interner Bericht, Fakultat Fur Informatik, Bernhard Beckert, Bernhard Beckert, Joachim Posegga, Joachim Posegga
The Prolog program "termexpansion((define C as A with B), (C=?A:-B,!)). termexpansion((transition E if C then D), ((transition E):-C,!,B,A,(transition))):-serialize(D,B,A)....
leantap: Lean tableau-based deduction (1995)
Bernhard Beckert, Joachim Posegga
prove((E;F),A,B,C,D):-!, prove(E,A,B,C,D), prove(F,A,B,C,D). prove(all(H,I),A,B,C,D):-!, "+length(C,D), copyterm((H,I,C),(G,F,C)), append(A,[all(H,I)],E), prove(F,E,B,[G---C],D)....
leanEA: A Poor Man's Evolving Algebra Compiler (1995)
Interner Bericht, Fakultat Fur Informatik, Bernhard Beckert, Bernhard Beckert, Joachim Posegga, Joachim Posegga
The Prolog program "termexpansion((define C as A with B), (C=?A:-B,!)). termexpansion((transition E if C then D), ((transition E):-C,!,B,A,(transition ))) :- serialize(D,B,A)....
leanEA: A Poor Man's Evolving Algebra Compiler, research report (1995)
Interner Bericht, Fakultät Für Informatik, Bernhard Beckert, Bernhard Beckert, Joachim Posegga, Joachim Posegga, ...
“term_expansion((define C as A with B), (C=>A:-B,!)). term_expansion((transition E if C then D), ((transition E):-C,!,B,A,(transition _))):serialize(D,B,A). serialize((E,F),(C,D),(A,B)):-...
Abstract Semantic Tableaux with Equality (1995)
This paper tries to identify the basic problems encountered in handling equality in the semantic tableau framework, and to describe the state of the art in solving these problems. The two main...
leanT A P : lean, tableau-based theorem proving (1994)
Bernhard Beckert, Joachim Posegga
prove((E;F),A,B,C,D):-!, prove(E,A,B,C,D), prove(F,A,B,C,D). prove(all(H,I),A,B,C,D):-!, "+length(C,D), copyterm((H,I,C),(G,F,C)), append(A,[all(H,I)],E), prove(F,E,B,[G---C],D)....
In this paper we describe how a combination of the classical "universal" E-unification and "rigid" E-unification, called "mixed " E-uni-fication, can be used to...
Adding equality to semantic tableaux (1994)
Abstract. This paper tries to identify the basic problems encountered in handling equality in the semantic tableau framework, and to describe the state of the art in solving these problems. The two...
3TAP - The Many-Valued Theorem-Prover (1994)
Reiner Hähnle, Bernhard Beckert, Stefan Gerberding
This is the 3 T A P handbook. 3 T A P is a many-valued tableau-based theorem prover developed at the University of Karlsruhe. The handbook serves a triple purpose: first, it documents the history and...
Bernhard Beckert, Reiner H, Anavai Ramesh, Neil V. Murray
. The concept of anti-link is defined, and useful equivalence-preserving operations on propositional formulas based on anti-links are introduced. These operations eliminate a potentially large number...
leanT A P : lean, tableau-based theorem proving (1994)
Bernhard Beckert, Joachim Posegga
prove((E;F),A,B,C,D):-!, prove(E,A,B,C,D), prove(F,A,B,C,D). prove(all(H,I),A,B,C,D):-!, \+length(C,D), copy_term((H,I,C),(G,F,C)), append(A,[all(H,I)],E), prove(F,E,B,[G|C],D)....
A completion-based method for mixed universal and rigid E-unification (1994)
Abstract. We present a completion-based method for handling a new version of E-unification, called “mixed ” E-unification, that is a combination of the classical “universal ” E-unification...
The even more liberalized δ-rule in free variable semantic tableaux (1993)
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Abstract. In this paper we have a closer look at one of the rules of the tableau calculus presented in [3], called the δ–rule, and the modification of this rule, that has been proved to be sound...
The tableau-based theorem prover 3TAP for multiple-valued logics (1992)
Beckert, Bernhard, Gerberding, Stefan, Haehnle, Reiner, Kernig, Werner
The tableau-based theorem prover 3TAP for multiple-valued logics. (1992)
Beckert, Bernhard, Gerberding, Stefan, Haehnle, Reiner, Kernig, Werner
The tableau-based theorem prover 3T A P for multiple-valued logics (1992)
Bernhard Beckert, Reiner Hähnle, Stefan Gerberding, Werner Kernig
3T A P is an acronym for 3–valued tableau–based theorem prover. It is based on the method of analytic tableaux. 3T A P has been developed at the University of Karlsruhe in cooperation with the...
An improved method for adding equality to free variable semantic tableaux (1992)
Bernhard Beckert, Reiner Hähnle
Abstract. Tableau–Based theorem provers can be extended to cover many of the nonclassical logics currently used in AI research. For both, classical and nonclassical first–order logic, equality is...