Inductive theorem proving is a topic of growing interest in the automated reasoning community. Following our successful first workshop in London 2013, we would like to invite you to a second workshop on inductive theorem proving. The workshop will be very informal and aims to give researchers interested in the topic a chance to meet, exchange ideas and perhaps also try out some of the available theorem provers. We would like to invite talks featuring demos and tutorials of inductive theorem provers, challenge problems, new directions of research or anything else of interest to the inductive theorem proving community.
Hope to see you in Gothenburg!
— The HipSpec crew
(Moa Johansson, Dan Rosén, Nick Smallbone, Koen Claessen)
The workshop will be free of charge but please register by filling in the form here. If you want to contribute a talk or demo, please submit a title and a short abstract when you register.
We’ll provide coffee but you’ll have to pay for lunch/dinner yourself.
Location and programme
The workshop will take place on Friday 20 March - Saturday 21 March at Chalmersvillan, Gibraltargatan 1A, Gothenburg, in the room upstairs:
Friday 20th March
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!
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: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
Saturday 21st March
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
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
Sweden doesn’t use Euros but Swedish Kronor.
The local airport is Gothenburg Landvetter, about 20 minutes from the city by taxi/airport bus. Once you’re in the city you can walk everywhere and Chalmers is about 20 minutes away by foot. The workshop is at Gibraltargatan 1A which you can see on the map above. Once you get in the building you should go upstairs.
If you want to use public transport, the easiest way is to buy a tourist card which you then scan when you get on the bus/tram. You can get these from many newsagents. Alternatively on the tram (but not the bus) you can pay onboard with a credit card; this gives you a ticket which is valid for 90 minutes on an unlimited number of journeys.
There are several ways to get the venue by public transport, listed below. The Västtrafik travel planner can help you work out a route.
By bus to Ålandsgatan
The easiest way is to take the bus to Ålandsgatan. This will drop you off on Gibraltargatan, almost outside the venue. The downside is that the stop is only on one bus line, and also that you can’t use a credit card to pay for a ticket onboard.
By tram/bus to Kapellplatsen
If you’re coming from town, you can get off at Kapellplatsen. If you got the tram, you’ll see a big crossroads and one of the roads will be Läraregatan, next to a large light-coloured building. If you get the bus, the bus stop is on Läraregatan. In any case, walk down Läraregatan until you get to an intersection. Turn right onto Gibraltargatan and you’ll see the building on the right.
By tram/bus to Chalmers
The venue is also near the Chalmers tram stop which is on several bus and tram lines. From the tram stop you can get to Chalmersvillan like so:
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.
On the day you can ring Nick Smallbone (+46 707 183 062) or Koen Claessen (+46 708 196 393).