DISPROVING on Wednesday, August 16th

Invited Talk (09:00‑10:00)

09:00‑10:00

Jian Zhang (Institute of Software, Chinese Academy of Sciences) Model and Counterexample Search: Successes and Challenges [pdf]

Session 1: Base technology (10:00‑10:30)

10:00‑10:30

Thomas Hillenbrand (Max-Planck-Institut für Informatik) Dalibor Topic (Max-Planck-Institut für Informatik) Christoph Weidenbach (Max-Planck-Institut für Informatik) Sudokus as Logical Puzzles Currently Sudoku puzzles are en vogue. More recently, several authors have shown how to solve these puzzles in under one second via propositional encodings. In constrast, first-order theorem proving is not assumed to be efficient on such problems. In this paper we present a ground-level encoding that is more compact than the propositional ones, and that our superposition- based theorem prover SPASS can cope with in the blink of an eye, which is confirmed by experimental evidence. A puzzle is solvable iff its encoding is satisfiable iff SPASS disproves that it entails the empty clause, by exhibiting a Herbrand model for it. Indeed disproving is effective here because SPASS always terminates on the formula class at hand. Furthermore we describe how to obtain an even more compact encoding using quantified variables, and define inference and reduction rules that can simulate the efficient behaviour of the ground encoding. The main motivation behind this study is to improve superposition-based techniques in the presence of finite sorts.

Break (10:30‑11:00)

Session 2: Base technology (11:00‑11:30)

11:00‑11:30

André Rognes (none) Automated relative consistency proving A way of presenting essential information about first order theories is introduced. The presentation allows for the automation of relative consistency proving for sentences from a known conservative reduction class for first order logic. Elements of the reduction class can be seen a way of presenting first order sentences in general. The theories are presented by algebras of partial polyadic signature, some of which correspond to consistent theories. A downward Löwenheim-Skolem type of result is shown in that first order sentences are satisfiable iff there is a satisfying interpretation of the sentence in a finite algebra corresponding to a consistent theory. This is also the case for infinity axioms, i.e. sentences that have infinite models only. An algorithm for extracting algebras from theories, presented by decision procedures, has been implemented. Moreover a disprover has been implemented utilising extracted algebras, a relative consistency prover and an introduced construction on algebras. In principle the disprover recognises any finitely satisfiable sentence. Moreover examples of infinity axioms, have been found that the disprover recognises in reasonable time, while various state-of-the-art semi-decision procedures do not.

Session 3: Verification (11:30‑12:30)

11:30‑12:00

Lee Pike (Galois Connections) Paul Miner (NASA Langley Research Center) Wilfredo Torres-Pomales (NASA Langley Research Center) Diagnosing a Failed Proof in Fault-Tolerance: A Disproving Challenge Problem This paper proposes a challenge problem in disproving. We describe a fault-tolerant distributed protocol designed at NASA for use in a fly-by-wire system for next-generation commercial aircraft. An early design of the protocol contains a subtle bug that is highly unlikely to be caught in faultinjection testing. We describe a failed proof of the protocol’s correctness in a mechanical theorem prover (PVS) with a complex unfinished proof conjecture. We use a model checking suite (SAL) to generate a concrete counterexample to the unproven conjecture to demonstrate the existence of a bug. However, we argue that the effort required in our approach is too high and propose what conditions a better solution would satisfy. We carefully describe the protocol and bug to provide a challenging but feasible case-study for disproving research.

12:00‑12:30

Markus Aderhold (Technische Universität Darmstadt) Christoph Walther (Technische Universität Darmstadt) Daniel Szallies (Technische Universität Darmstadt) Andreas Schlosser (Technische Universität Darmstadt) A Fast Disprover for VeriFun We present a disprover for universal formulas stating conjectures about functional programs. The quantified variables range over freely generated polymorphic data types, thus the domains of discourse are infinite in general. The objective in the development was to quickly find counter-examples for as many false conjectures as possible, without wasting too much time on true statements. We present the reasoning method underlying the disprover and illustrate its practical value in several applications in an experimental version of the verification tool VeriFun.

Lunch break (12:30‑14:00)

Invited Talk (14:00‑15:00)

14:00‑15:00

Silvio Ranise (LORIA-INRIA-Lorraine & Università degli Studi di Milano) Satisfiability Solving for Program Verification: towards the efficient combination of Automated Theorem Provers and Satisfiability Modulo Theory Tools [pdf]

Session 4: Verification (15:00‑15:30)

15:00‑15:30

Louise Abigail Dennis (University of Nottingham) Program Slicing and Middle-Out Reasoning for Error Location and Repair This paper describes a proof-based approach to the location and repair of errors in functional programs. The approach is based on the use of program slicing to locate errors and middle-out reasoning to repair them. An implementation in the lclam proof planning system is described with some preliminary results.

Break (15:30‑16:00)

Session 5: Base Technology (16:00‑17:00)

16:00‑16:30

Mahadevan Subramaniam (University of Nebraska at Omaha) Deepak Kapur (UNM) Stephan Falke (University of New Mexico) Predicting Failures of Inductive Proof Attempts Reasoning about recursively defined data structures and functions defined on them typically requires proofs by induction. Despite advances made in automating inductive reasoning, proof attempts by theorem provers frequently fail while performing inductive reasoning. A user of such a system must scrutinize a failed proof attempt and do intensive debugging to understand the cause of failure. The failure of proof attempts could be because of a number of reasons even when a conjecture is believed to be valid. An induction scheme used in a proof attempt is not powerful enough to yield useful induction hypotheses which can be applied effectively. A proof attempt needs intermediate lemmas. The focus of the research reported in this paper is to analyze possible failures of proof attempts due to inapplicability of induction hypotheses and predict failure a priori before even attempting a proof, so as to avoid failed attempts. Definitions of functions appearing in a conjecture are analyzed to determine whether their interaction in the conjecture is guaranteed for a proof attempt to get stuck. The analysis relies on the concept of blocking of a function definition by another function definition. If in a conjecture, a function $g$ appears as an argument to another function $f$ such that when the definition of $g$ is expanded, $f$ blocks a function symbol resulting from the definition of $g$, then a proof attempt of the conjecture based on expanding the definition of $g$ is likely to get stuck. The concept of a flawed induction scheme is introduced capturing this idea. It is shown that if a proof of a conjecture is attempted using only flawed induction schemes, then under certain conditions, such proof attempts are guaranteed to fail. The analysis can be easily automated and is illustrated on several examples.

16:30‑17:00

Peter Baumgartner (National ICT Australia (NICTA)) Alexander Fuchs (University of Iowa) Cesare Tinelli (University of Iowa) Hans de Nivelle (Max-Planck Institut fuer Informatik) Computing Finite Models by Reduction to Function-Free Clause Logic Recent years have seen considerable interest in procedures for computing finite models of first-order logic specifications. One of the major paradigms, MACE-style model building, is based on reducing model search to a sequence of propositional satisfiability problems and applying (efficient) SAT solvers to them. A problem with this method is that it does not scale well, as the propositional formulas to be considered may become very large. We propose instead to reduce model search to a sequence of satisfiability problems made of function-free first-order clause sets, and to apply (efficient) theorem provers capable of deciding such problems. The main appeal of this method is that first-order clause sets grow more slowly than their propositional counterparts, thus allowing for more space efficient reasoning. In the paper we describe the method in detail and show how it is integrated into one such prover, Darwin, our implementation of the Model Evolution calculus. The results are general, however, as our approach can used in principle with any system that decides the satisfiability of function-free first-order clause sets. To demonstrate its practical feasibility, we tested our approach on all satisfiable problems from the TPTP library. Our methods can solve a significant subset of these problem, which overlaps but is not included in the subset of problems solvable by state-of-the-art finite model builders such as Paradox and Mace4.