Second European Workshop on
Higher-Order Automated Reasoning
11–14 June 2019, Amsterdam, The Netherlands
The Matryoshka workshop brings together researchers working on automated deductive techniques for higher-order logics (especially simple type theory and dependent type theory). There has been much progress in recent years with the higher-order automatic theorem provers Leo-III and Satallax, the Lean proof assistant, and metaprovers such as HOLyHammer and Sledgehammer.
With the Matryoshka project, we aim at designing a new generation of higher-order automatic theorem provers based on state-of-the-art first-order provers, including E, veriT, and CVC4, and to integrate them in popular proof assistants. We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. We encourage researchers motivated by the same goals to get in touch with us, subscribe to the matryoshka-devel mailing list, and join forces.
The workshop is a successor of the LPAR-05 workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), held in Montego Bay, Jamaica. The Matryoshka workshop series is conceived to be a meeting point for the Matryoshka team and colleagues working on the same challenge. It is an informal event. We expect to hold it at least once a year until the project's completion in 2022.
This year, the workshop joins forces with the VeriDis group's retreat. The VeriDis project aims to exploit and further develop the advances and integration of interactive and automated theorem proving applied to the area of concurrent and distributed systems. The goal of our project is to assist algorithm and system designers to carry out formally proved developments, where proofs of relevant properties as well as bugs can be found fully automatically.
The workshop will take place from Tuesday the 11 June to Friday the 14 June at the Vrije Universiteit Amsterdam. The VU is easily accessible on foot from the Amsterdam Zuid station, a short train ride away from Amsterdam Airport Schiphol. There are also parking spaces. See How to get to VU Amsterdam for details.
The workshop will slowly start on 11 June from 13:00 in room 6A04 on the 6th floor of the OZW building. The sessions on Wednesday are in room 7B01 of the same building. On Tuesday only the morning session is in room 6A04 of the OZW building. The afternoon session and the session on Friday is in room M623 of the W&N building. The workshop ends on Friday the 14 June at 12:30.
Hotels in Amsterdam can be very expensive. Even the cheapest options often cost over 100 euros per night. The neighboring city of Amstelveen has more reasonably priced options (e.g., Ibis) and is located close to the VU campus, a few stops away by public transportation (tram line 5 or metro line 51).
Tuesday 11 June (Room 6A04, OZW building)
Arrival & Welcome
VeriDis Session 1
Distributed algorithms are known to be hard to design and verify.
Refining abstract models into less abstract models has been
successfully used to design correct-by-construction distributed
algorithms. In this talk, I will present you a systematic way of
transforming Event-B models of distributed algorithm into DistAlgo
programs. The presentation will consist of an illustration of
this transformation on an example: the stop-and-wait ARQ.
SPASS-SATT is a CDCL(LA) solver for linear rational and linear
mixed/integerarithmetic. This system description explains its specific
features: fast cube tests for integer solvability, bounding
transformations for unbounded problems, close interaction between the
SAT solver and the theory solver,efficient data structures,
andsmall-clause-normal-form generation. SPASS-SATT is currently one of
thestrongest systems on the respective SMT-LIB benchmarks.
SimGrid is a tool for the simulation of distributed programs, designed
to be reproducible and requiring a full knowledge of the distributed
system. However, in real-life scenarios we only have an average
guarantee, such as the availability. The goal of this work in progress
is to enhance SimGrid with stochastic features, allowing the description
of such systems, and then to implement a statistical model-checker in
order to estimate performance indices for the distributed program.
|Group dinner at Wagamama at Zuidplein 12
Wednesday 12 June (Room 7B01, OZW building)
VeriDis Session 2
We consider the problem whether termination of affine integer loops is
decidable. Since Tiwari conjectured decidability in 2004, only special
cases have been solved. We complement this work by proving decidability
for the case that the update matrix is triangular.
Algorithms for Zero-Dimensional Polynomial Systems
SCL – Clause Learning from Simple Models
VeriDis Session 3
HOπ in Coq
Group lunch at Grand Café De Bosbaan at Bosbaan 4
VeriDis Session 4
Automated reasoning tools have becomes very powerful in the last two
decades. To solve a given problem using such tools, it
must be encoded into a representation that is suitable for automated
reasoning. Our ability to solve the problem depends heavily on the
quality of the encoding.
TLA+ is a language for formal specification of all kinds of computer systems.
System designers use this language to specify concurrent, distributed, and
fault-tolerant protocols, which are traditionally presented in pseudo-code.
TLA+ is extremely concise yet expressive: The language primitives include
Booleans, integers, functions, tuples, records, sequences, and sets thereof,
which can be also nested. This is probably why the only model checker for TLA+
(called TLC) relies on explicit enumeration of values and states.
Automated theorem provers are now commonly used within interactive
theorem provers to discharge an increasingly large number of
proof obligations. To maintain the trustworthiness of a proof,
the automatically found proof must be verified inside the proof
assistant. We present here a reconstruction procedure in the proof assistant
Isabelle/HOL for proofs generated by
the satisfiability modulo theories solver veriT
which is part of the smt tactic.
Checking the soundness of the cyclic induction reasoning for first-order
logic with inductive definitions (FOLID) may be costly; the standard
checking method is decidable but based on a doubly exponential
complement operation for Büchi automata. In this talk, I will present
a semi-decidable polynomial method whose most expensive steps recall
the comparisons with multiset path orderings. In practice, it has been
integrated in the Cyclist prover and successfully checked all the proofs
generated with the standard method and included in its distribution.
|Free time to explore the city
|Group dinner at Sama Sebo at P.C. Hooftstraat 27
Thursday 13 June morning (Room 6A04, OZW building)
VeriDis+Matryoshka Joint Session 1
I have recently extended my formalisation of CDCL such that it can find
an optimal model that minimise the weight of its literals. This calculus
was formalised in Isabelle, but it is not able to find optimal partial
models. Therefore, we used an encoding that reduces the search for an
optimal partial model to the search for an optimal total model.
SMT solvers are among the most suited tools for quantifier-free
first-order problems, and their support for quantified formulas has been
improving in recent years. To instantiate quantifiers, they rely on
heuristic techniques that generate thousands of instances, most of them
useless. We propose to apply state-of-the-art machine learning
techniques as classifiers for instances on top of the instantiation
process. We show that such techniquescan indeed decrease the number of
generated useless instances. We envision that this couldlead to more
efficient SMT solving for quantified problems.
TLA+ is a specification language based on set theory. Unlike most
formal languages, TLA+ is untyped, a design principle mainly motivated
by flexibility, convenience and expressiveness. TLA+'s interactive
prover, TLAPS, relies on back-end provers to treat proof obligations. In
previous work, an encoding of TLA+'s set theory into first-order logic
was defined in order to provide support for SMT solvers. In this
presentation, we will motivate the extension of this work to
|Lunch on our own (cafeteria, Loetje, ...)
Thursday 13 June afternoon (Room M623, W&N building)
Matryoshka Session 1
We designed a complete superposition calculus for a clausal
fragment of extensional polymorphic higher-order logic that includes
anonymous functions but excludes Booleans. We implemented the calculus
in the Zipperposition prover and evaluated it on TPTP and Isabelle
Normalizing casts inside expressions
The lean elaborator implements a coercion mechanism, which
automatically adds casts inside expressions. This can be as
frustrating as it is usefull, since users sometimes end up
struggling with very simple statements because they have to
manually move these casts around. In this talk I will present
my work on norm_cast, a light-weight and extensible tactic
aimed at making this process more intuitive.
Matryoshka Session 2
Higher order unification has usually been regarded as one of
the algorithms whose search space is hard to control. In this
talk, I will present some ways in which the unifier search can
be kept under control. Our initial experiments show significant
improvements compared to commonly used algorithms.
I present ongoing research on the use of a non-monotonic ordering that
orients combinator axiom left-to-right to parametise the superposition
calculus. Building on work carried out by the Matryoshka team, I explore
tuning the calculus's side conditions to maintain completeness.
Friday 14 June (Room M623, W&N building)
Matryoshka Session 3
This talk is about the journey of a Lean newbie formalising basic
theorems about continued fractions. Like every interesting journey, also
mine had ups and downs. I will talk about both of them, the lessons I
learnt, and the Lean features I am missing.
Remarkable work has recently been done to make first-order
superposition based provers to support boolean subterms. In
this talk we review several ways to support booleans. We also
address other aspects of higher order reasoning with booleans
such as axiom of choice and primitive substitutions. Our
evaluation shows promising results.
Matryoshka Session 4
|Lunch on our own (cafeteria, Loetje, ...)
Alexander Bentkamp* (VU Amsterdam)
Ahmed Bhayat* (University of Manchester)
Manon Blanc (ENS Paris-Saclay and Inria Nancy)
Jasmin Blanchette (VU Amsterdam)
Martin Bromberger* (MPII Saarbrücken)
Horatiu Cirstea (Inria Nancy)
Antoine Defourné* (Inria Nancy)
Yann Duplouy* (Inria Nancy)
Daniel El Ouraoui* (U. Lorraine and Inria Nancy)
Alberto Fiori* (MPII Saarbrücken)
Mathias Fleury* (MPII Saarbrücken)
Pascal Fontaine (U. Lorraine)
Florian Frohn* (MPII Saarbrücken)
Alexis Grall* (Inria Nancy)
Marijn Heule* (U. Texas at Austin)
Kevin Kappelmann* (VU Amsterdam)
Igor Konnov* (Inria Nancy)
Sergueï Lenglet* (Inria Nancy)
Paul-Nicolas Madelaine* (ENS Paris & VU Amsterdam)
Stephan Merz (Inria Nancy)
Visa Nummelin* (VU Amsterdam)
Hamid Rahkooy* (Inria Nancy)
Hans-Jörg Schurr* (U. Lorraine and Inria Nancy)
Sorin Stratulat* (U. Lorraine)
Sophie Tourret (MPII Saarbrücken)
Petar Vukmirović* (VU Amsterdam)
Uwe Waldmann (MPII Saarbrücken)
Christoph Weidenbach (MPII Saarbrücken)
This workshop is partially supported by the ERC Starting Grant 2016 Matryoshka (grant agreement No.
and by the NWO incidentele steun scheme.
We kindly ask participants to mention the support from the ERC and the NWO
in publications or in other kinds of scientific output that directly follows
from the workshop. (The NWO would also like to receive a copy of the relevant
|This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement No. 713999.