The Second Workshop on Automated Inductive Theorem-proving (WAIT?),
20-21 March 2015, Chalmers University, Gothenburg, Sweden

9:00: Coffee and welcome

9:30: Rustan Leino, Microsoft Research
Induction, synthesis, inference
In this talk, I will sketch some similarities between induction, synthesis, and inference. Might we be able to reuse techniques across these areas? I’ll use some demos to support my position.

10:00: Gudmund Grov, Heriot-Watt University
A new project: tactics for the Dafny program verifier
Recently, there has been a wave of auto-active program verifiers. These share the characteristics of using an automated theorem prover for the verification conditions, and the user only works with the program text. If a correct program fails to verify, the user needs to provide additional guidance in the program text, e.g. in terms of contracts, annotations and ghost constructs. Within interactive theorem provers, it is common to reduce user-interaction by encoding common reasoning patterns within special proof methods called "tactics". Inspired by such tactics, this talk will introduce a new project that will enable users to encode proof patterns for the Dafny program verifier as "Dafny tactics"; and using Dafny to encoding them. The vision is that low-level and repetitive details, often resulting from a trial-and-error process, can be encoded as higher-level Dafny tactics. These tactics can then be reused for similar tasks, liberating users from low-level search tasks.

10:30: Simon Robillard, Chalmers
Generating Invariants of Java Programs Using a Theorem Prover
The main obstacle to verifying properties of imperative programs stems from the expressiveness of loop constructs. While explicit inductive reasoning is a possible approach, it is often more natural to use loop invariants. Users of verification tools are typically expected to provide such invariants, e.g. by annotating the program being verified.
The theorem prover Vampire now includes a feature harnessing the power of its calculus to generate invariants from a loop description, without the need for user guidance. The strength of this method, compared to existing techniques, lies in its ability to produce invariants containing alternations of quantifiers.
The next challenge is to use this feature on an industrial language, namely Java. This is being accomplished by integrating Vampire’s invariant generation into the KeY verification system.

11:00: Tons of inductive problems + working session
We HipSpeccers have recently been working on TIP, a benchmark suite for automated induction, to make it easier to compare different tools: https://github.com/tip-org/benchmarks.
While we have made all the design decisions ourselves so far, we of course want the community to have a say in the direction and development of TIP. We will introduce the benchmark suite and then have a discussion for people to voice their opinions.
The benchmark suite also includes some challenge problems that no-one has proved automatically, to the best of our knowledge. It would be fun if people try them on their tools during the workshop and see what happens!

12:00: Lunch

13:15: Moa Johansson, Chalmers
Docent lecture (promotion lecture):
Inductive Theorem Proving and Theory Exploration
My research is about automating inductive proofs with applications in for example verification of functional programs. However, induction is undecidable, meaning that we can never write a computer program that guarantees to always find a proof, even though one exists. For example, the proof might need a lemma, which itself requires a new induction and so on. Despite this, many proofs can still be automated, especially if we equip the theorem proving program with some more creative capabilities, that otherwise often are left to a human expert user. I’m interested in how we can build a theorem prover which manage to perform the more creative “eureka”-steps, such as finding the key lemma that makes a proof go through. For this, we are developing a method called Theory Exploration, which uses testing and clever heuristics to discover new lemmas describing properties about computer programs.

14:30: Stefan Hetzl, Vienna University of Technology
Inductive theorem proving based on tree grammars
I will speak about an approach to inductive theorem proving which is based on recent proof-theoretic results on the relationship between induction and tree grammars.
This approach suggests an algorithm for proving universal statements by induction which proceeds in two phases: the first phase consists of a structural analysis of proofs of instances of the universal statement. The result of such an analysis is a tree grammar which induces a quantifier-free logical unification problem. Each solution to this problem is an induction invariant. The second phase consists of finding a solution of this unification problem.
I will illustrate this technique by well-known examples from the literature.

15:00: Irene Lobo Valbuena, Chalmers
Conditional laws in Hipster

15:15: Coffee

15:45: Nick Smallbone, Chalmers
QuickSpec 2, a fast theory exploration tool
One important part of automated induction is finding the right lemmas. Our tool QuickSpec finds properties of functional programs by testing. It is used in our prover HipSpec to discover lemmas but is also a useful tool for program understanding in its own right. We have recently redesigned QuickSpec so that it works on much more difficult problems; I will show the new version on some hard examples and explain how it works.

16:15: Dan Rosén, Chalmers
Context Free Grammars and Induction
Showing that a Context Free Grammar is unambiguous can be expressed as an induction problem over a functional program. The corresponding program uses plain, simple structural induction. On the other hand, the proof of unambiguity can require complex lemmas about functions that are not present in the original program. This is way beyond what HipSpec can do automatically, so the demos will show HipSpec used in a more interactive setting.

16:45: Day ends, but people can stay and work if they want to

19:00: Workshop dinner at Smaka
Smaka, Vasaplatsen 3, http://goo.gl/maps/9EmMj
Menu: http://smaka.se/eng_meny.html

9:00: Coffee

9:15: Koen Claessen, Chalmers
Bounded Model Checking of Functional Programs
We show how we can use a SAT-solver to find counter examples to properties of functional programs. The method consists of a combination of symbolic evaluation and bounded model checking.

9:45: Andrew Reynolds, EPFL
Using CVC4 for Proofs by Induction in SMT
Satisfiability modulo theory solvers are increasingly being used to solve quantified formulas over structures such as integers and term algebras. This talk presents a set of techniques that introduce inductive reasoning into SMT solving algorithms that is sound with respect to the interpretation of structures in SMT-LIB standard. The techniques include inductive strengthening of conjecture to be proven, as well as facility to automatically discover subgoals during an inductive proof, where subgoals themselves can be proven using induction. We demonstrate an implementation of these techniques in the SMT solver CVC4, focusing both on how problems for datatypes such as lists, sets, and binary trees are encoded in the SMT-LIB standard, and how they are handled by the solver. Finally, we discuss the impact of different encodings on the performance of inductive reasoning in SMT, in particular, showing that the native theory reasoning capabilities of an SMT solver can be leveraged for inductive proofs.

10:15: Daniel Wand, Max Planck Institute for Informatics
Induction in superposition

10:45: Coffee

11:00: Jasmin Blanchette, Inria, LORIA, MPI-Inf.
Extending Sledgehammer with Induction Provers
Sledgehammer, MizAR, HOLyHammer, and similar tools exploit first-order automatic theorem provers (ATP) to solve goals that arise in interactive proofs. They rely on the ATP output, e.g. a detailed proof or an unsat core, to reconstruct the proof in the proof assistant. In this talk, I describe preliminary work on integrating Daniel Wand’s superposition-con-induction provers in Isabelle.

11:15: Reuben Rowe
Reuben talked about his new project on cyclic proofs. Here are some links:

11:30: Jesper Bengtsson

11:45: working session

12:15: Report on challenge problems + final discussion

13:00: end

Walk under the big Chalmers sign and go up the big steps to the left.

Carry on to the end of the path. There will be a road running from left to right, which is Gibraltargatan.

Turn left onto Gibraltargatan. Chalmersvillan is on the left after a couple of minutes, Gibraltargatan 1A.