Christoph Walther

LPAR Conference 2005 Conference Paper

Reasoning About Incompletely Defined Programs

• Christoph Walther
• Stephan Schweitzer

Abstract We consider automated reasoning about recursive partial functions with decidable domain, i. e. functions computed by incompletely defined but terminating functional programs. Incomplete definitions provide an elegant and easy way to write and to reason about programs which may halt with a run time error by throwing an exception or printing an error message, e. g. when attempting to divide by zero. We investigate the semantics of incompletely defined programs, define an interpreter for those programs and discuss the termination of incompletely defined procedures. We then analyze which problems need to be solved if a theorem prover designed for verification of completely defined programs is modified to work for incompletely defined programs as well. We also discuss how to reason about stuck computations which arise when calling incompletely defined procedures with invalid arguments. Our method of automated reasoning about incompletely defined programs has been implemented in the verification tool \(\surd{\rm eriFun}\). We conclude by discussing experiences obtained in several case studies with this implementation and also compare and relate our proposal to other work.

LPAR Conference 2004 Conference Paper

Automated Termination Analysis for Incompletely Defined Programs

• Christoph Walther
• Stephan Schweitzer

Abstract Incompletely defined programs provide an elegant and easy way to write and to reason about programs which may halt with a run time error by throwing an exception or printing an error message, e. g. when attempting to divide by zero. Due to the presence of stuck computations, which arise when calling incompletely defined procedures with invalid arguments, we cannot use the method of argument bounded algorithms for proving termination by machine. We analyze the problem and present a solution to improve this termination analysis method so that it works for incompletely defined programs as well. Our technique of proving the termination of incompletely defined programs maintains performance as well as simplicity of the original method and proved successful by an implementation in the verification tool \(\surd\) eriFun.

LPAR Conference 2003 Conference Paper

A Machine-Verified Code Generator

• Christoph Walther
• Stephan Schweitzer

We consider the machine-supported verification of a code generator computing machine code from WHILE -programs, i. e. abstract syntax trees which may be obtained by a parser from programs of an imperative programming language. We motivate the representation of states developed for the verification, which is crucial for success, as the interpretation of tree-structured WHILE -programs differs significantly in its operation from the interpretation of the linear machine code. This work has been developed for a course to demonstrate to the students the support gained by computer-aided verification in a central subject of computer science, boiled down to the classroom-level. We report about the insights obtained into the properties of machine code as well as the challenges and efforts encountered when verifying the correctness of the code generator. We also illustrate the performance of the \(\checkmark\) eriFun system that was used for this work.

I&C Journal 2000 Journal Article

On Terminating Lemma Speculations

• Christoph Walther
• Thomas Kolbe

The improvement of theorem provers by reusing previously computed proofs is investigated. A method for reusing proofs is formulated as an instance of the problem reduction paradigm such that lemmata are speculated as proof obligations, being subject for subsequent reuse attempts. We motivate and develop a termination requirement, prove its soundness, and show that the reusability of proofs is not spoiled by the termination requirement imposed on the reuse procedure. Additional evidence for the general usefulness of the proposed termination order is given for lemma speculation in induction theorem proving.

AIJ Journal 2000 Journal Article

Proving theorems by reuse

• Christoph Walther
• Thomas Kolbe

We investigate the improvement of theorem proving by reusing previously computed proofs. We have developed and implemented the Plagiator system which proves theorems by mathematical induction with the aid of a human advisor: If a base or step formula is submitted to the system, it tries to reuse a proof of a previously verified formula. If successful, labour is saved, because the number of required user interactions is decreased. Otherwise the human advisor is called for providing a hand crafted proof for such a formula, which subsequently—after some (automated) preparation steps—is stored in the system's memory, to be in stock for future reasoning problems. Besides the potential savings of resources, the performance of the overall system is improved, because necessary lemmata might be speculated as the result of an attempt to reuse a proof. The success of the approach is based on our techniques for preparing given proofs as well as by our methods for retrieval and adaptation of reuse candidates which are promising for future proof reuses. We prove the soundness of our approach and illustrate its performance with several examples.

IJCAI Conference 1995 Conference Paper

Second-Order Matching modulo Evaluation A Technique for Reusing Proofs

• Thomas Kolbe
• Christoph Walther

AIJ Journal 1994 Journal Article

On proving the termination of algorithms by machine

• Christoph Walther

Proving the termination of a recursively defined algorithm requires a certain creativity of the (human or automated) reasoner for inventing a hypothesis whose truth implies that the algorithm terminates. We present a reasoning method for simulating this kind of creativity by machine. The proposed method works automatically, i. e. without any human support. We show, (1) how a termination hypothesis for an algorithm is synthesized by machine, (2) which knowledge about algorithms is required for an automated synthesis, and (3) how this knowledge is computed. Our method solves the problem for a relevant class of algorithms, including classical sorting algorithms and algorithms for standard arithmetical operations, which are given in a pure functional notation. The soundness of the method is proved and several examples are presented for illustrating the performance of the proposal. The method has been implemented and proved successful in practice.

ECAI Conference 1994 Conference Paper

Reusing Proofs

• Thomas Kolbe
• Christoph Walther

IJCAI Conference 1993 Conference Paper

Combining Induction Axioms by Machine

• Christoph Walther

The combination of induction axioms is investigated. It is shown how a pair of competing induction axioms (which e. g. are suggested by a heuristic of an induction theorem prover on a specific verification problem) are combined yielding a new induction axiom. The relation implicitly defined by the new axiom is the set-theoretic union of the well-founded relations implicitly defined by the induction axioms initially given. The proposed approach is non-heuristic but safe in the sense that an induction proof with the new axiom can be obtained whenever an induction proof with one of the given axioms would have been successful. Based on a result of Bachmair and Dershowitz for proving term rewriting systems noctherian, a commutation test is developed as a deductive requirement to verify the soundness of the combined axiom: It is shown how so-called commutation formulas can be derived by machine from the given axioms such that a verification of these formulas (e. g. by an induction theorem prover) guarantees the well-foundcdness of the relation defined by the combined axiom. Examples are presented to demonstrate the usefulness and strength of the proposed technique.

LPAR Conference 1992 Conference Paper

Computing Induction Axioms

• Christoph Walther

Abstract The computation of induction axioms in the explicit induction paradigm is investigated. A simple notion with a well-defined semantics, called a relation description, is proposed as the elementary building block for automated reasoning on induction axioms. It is demonstrated how relation descriptions can be created, manipulated and compared by machine so that useful and strong induction axioms can be derived from them. For each of these operations the semantics of their effects and a precise semantical justification for their application is given. It is shown how the proposed framework can be used to describe the methods implemented in Boyer and Moore's NQTHM system in an abstract setting with a well-defined semantics. NQTHM's merging and subsumption heuristics for combining and comparing induction schemas arc analysed as an example, how a rigorous formal approach may uncover implicit assumptions and hidden flaws. A containment test then is proposed as a powerful, non-heuristic, and completeness preserving operation to select among competing induction schemas. The motivation for this test evolves straightforwardly in the given-framework by recognizing the semantics of the intended effect

AIJ Journal 1985 Journal Article

A mechanical solution of Schubert's Steamroller by many-sorted resolution

• Christoph Walther

We demonstrate the advantage of using a many-sorted resolution calculus by a mechanical solution of a challenge problem. This problem known as ‘Schubert's Steamroller’ had been unsolved by automated theorem provers before. Our solution clearly demonstrates the power of a many-sorted resolution calculus. The proposed method is applicable to all resolution-based inference systems.

ECAI Conference 1985 Conference Paper

Unification in Many-Sorted Theories

• Christoph Walther

AAAI Conference 1984 Conference Paper

A Mechanical Solution of Schubert’s Steamroller by Many-Sorted Resolution

• Christoph Walther

We demonstrate the advantage of using a many-sorted resolution calculus by a mechanical solution of a challenge problem. This problem known as "Schubert’s Steamroller" had been unsolved by automated theorem provers until now. Our solution clearly demonstrates the power of a many-sorted resolution calculus. The proposed method is applicable to all resolution-based inference systems.

IJCAI Conference 1983 Conference Paper

A Many-Sorted Calculus Based on Resolution and Paramodulation

• Christoph Walther