| Jürgen Giesl. Disproving Termination of Term Rewriting |
| Abstract: We focus on the termination analysis of term rewrite systems (TRSs), since term rewriting provides a general mechanism to model evaluation in different programming languages. Therefore, techniques for termination analysis of TRSs can often be adapted to other programming languages afterwards. However, almost all existing techniques for automated termination analysis try to prove termination and there are hardly any methods to prove non-termination. In this work, we introduce techniques to disprove termination of TRSs within the so-called dependency pair framework. Apart from disproving full termination, we also present new methods which can disprove termination under the innermost evaluation strategy (i.e., they can disprove innermost termination). Innermost termination is particularly important in practice, since it corresponds to termination under the eager call-by-value evaluation strategy used in many programming languages. The benefits of our results are twofold. First, detecting non-termination automatically can be very helpful for software development when debugging programs. Second, we show that combining termination and non-termination techniques within the dependency pair framework is particularly useful: On the one hand, termination techniques also help for disproving termination, because they identify those parts of a TRS which may cause non-termination. On the other hand, non-termination techniques are helpful for proving termination, because they can detect "dead ends" during a termination proof attempt. We implemented and evaluated our contributions in the automated termination prover AProVE. Due to these results, AProVE was the winning tool in the International Competition of Termination Provers 2005, both for proving and for disproving (innermost) termination of term rewriting. The talk is based on joint work with Rene Thiemann and Peter Schneider-Kamp. |
| Aaron Stump. Validated Construction of Congruence Closures |
| Abstract: It is by now well known that congruence closure (CC) algorithms can be viewed as implementing ground completion: given a set of ground equations, the CC algorithm computes a convergent rewrite system whose equational theory conservatively extends that of the original set of equations. We call such a rewrite system a CC for the original set. This paper describes work in progress to create an implementation of a CC algorithm which is validated, in the following sense. Any non-aborting, terminating run of the implementation is guaranteed to produce a CC for the input set of equations. Note that aborting or failing to terminate can happen for implementations of CC algorithms only due to bugs in code; the algorithms themselves are usually proved terminating and correct. Validation of an implementation of a CC algorithm is achieved by implementing the algorithm in RSP1, a dependently typed programming language. Type checking ensures that proofs of convergence and conservative extension are well-formed. |
| Moussa Demba, Francis Alexandre and Khaled Bsaies. Correction of faulty conjectures and programs extraction |
| Abstract: We present a method for patching faulty conjectures in automatic theorem proving. The method is based on well-known folding/unfolding rules \cite{BUR2}. Theconjectures we are interested in here are implicative formulas that are of the following form: \forall x (\exists Y\Gamma(x,Y)<= \Delta(x)). A faultyconjecture is a statement \forall x\phi(x), which is not provable in some given program T, defining all the predicates occurring in\phi, i.e, M(T)\not \models \phi, where M(T means the least Herbrand model of T, but it would be if enough conditions, say P, were assumed to hold, i.e., M(T\cup Q)\models (\phi<=P), where Q is a definition of P. |
| Marc Bezem. Disproving Distributivity in Lattices Using Geometric Logic Geometric Logic |
| Abstract: We report on experiments finding countermodels with a theorem prover for geometric logic. The main insight we acquire here is that it can be necessary to strengthen the geometric theory in order to find certain models. More precisely, we have added to the the theory of lattices an equality theory which enforces the system to consider quotients of the syntactical models. In this way our system recovered the two minimal 5-point lattices which are not distributive. One of these is modular and the other is not. Disproving distributivity in modular lattices has been the most demanding test so far. We discuss the results and some variations on the equality theme. |
| Philipp Ruemmer. Generating Counterexamples for Java Dynamic Logic |
| Abstract: First-Order Dynamic Logic is an extension of First-Order Predicate Logic that enables propositions about programs to be made in a natural way. The adherence of a program to certain properties---like preserving invariants or compliance with pre-/postconditions---can be translated into the statement that a particular formula of Dynamic Logic is valid, which can be proved mechanically using calculi. Accordingly, dealing with programs that violate a formal specification leads to the investigation of invalid formulas. We consider a dynamic logic for Java and describe an approach for proving formulas invalid that works by reduction to the validity problem. Furthermore, the method allows to derive concrete counterexamples for validity, which could be a useful tool for debugging programs or specifications. |
| Byron Cook. Automatic Theorem Proving for Program Verification Engines |
| Abstract: Microsoft has made an extensive investment in the area of software model checking. Tools such as Slam, Zing, KIS, Terminator, and ESP are now being used both inside and outside of the company. In this talk I will describe some of the underlying automatic theorem proving infrastructure used by these verification tools. I will also describe some recent advances and findings in this area. |