VeriDis Retreat
Matryoshka 2019

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.

Please send an email to Pascal Fontaine and Hans-Jörg Schurr if you would like to give a talk, demonstrate a tool, or otherwise participate.

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


Coffee break

VeriDis Session 1


Integration of Event-B and Distalgo
Alexis Grall

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.


Martin Bromberger

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.


Statistical Verification of Distributed Programs Within SimGrid
Yann Duplouy

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.



18:30–20:30Group dinner at Wagamama at Zuidplein 12

Wednesday 12 June (Room 7B01, OZW building)

VeriDis Session 2


Termination of Triangular Integer Loops is Decidable
Florian Frohn

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
Hamid Rahkooy


SCL – Clause Learning from Simple Models
Alberto Fiori


Coffee break

VeriDis Session 3


HOπ in Coq
Sergueï Lenglet




Group lunch at Grand Café De Bosbaan at Bosbaan 4

VeriDis Session 4


Encoding Challenges for Hard Problems
Marijn Heule

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.
In this talk we discuss some progress and challenges to construct a high-quality encoding for two long-standing open problems: efficient matrix multiplication and the Collatz conjecture. We propose to encode both problems into propositional logic. We weaken the matrix multiplication problem to ensure a much more compact representation. For the Collatz conjecture, which is a halting problem and therefore not in NP, we search for a ranking function using term rewriting termination techniques.


Making TLA+ model checking symbolic
Joint work with Jure Kukovec and Thanh Hai Tran (TU Wien, Austria)
Igor Konnov

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.
In this talk, we present a first symbolic model checker for TLA+. Like TLC, it assumes that all specification parameters are fixed and all states are finite structures. Unlike TLC, our model checker translates the underlying transition relation into quantifier-free SMT constraints, which allows us to exploit the power of SMT solvers.

16:00–16:30Coffee break

Reconstructing veriT proofs in Isabelle/HOL
Hans-Jörg Schurr
Joint work with Mathias Fleury

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.
We describe the architecture of our improved reconstruction method and the challenges we faced in designing it. Our experiments show that the veriT-powered smt tactic is regularly suggested by Sledgehammer as the fastest method to automatically solve proof goals.


Efficient Validation of FOLID Cyclic Induction Reasoning
Sorin Stratulat

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.
FOLID cyclic proofs may also be hard to certify. Our method helps to represent the cyclic induction reasoning as being well-founded, where the ordering constraints are automatically built from the analysis of the proofs. Hence, it creates a bridge between the two induction reasoning methods and opens the perspective to use the certification methods adapted for well-founded induction proofs.

17:30–19:30Free time to explore the city
19:30–21:30Group dinner at Sama Sebo at P.C. Hooftstraat 27

Thursday 13 June morning (Room 6A04, OZW building)

VeriDis+Matryoshka Joint Session 1


Extending an Isabelle Formalisation of CDCL to Optimising CDCL
Mathias Fleury

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.


Machine Learning for Instance Selection in SMT Solving
Daniel El Ouraoui

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.


Leveraging Automatic Deduction for Verification
Antoine Defourné

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 higher-order solvers.


Coffee break

12:00–14:00Lunch on our own (cafeteria, Loetje, ...)

Thursday 13 June afternoon (Room M623, W&N building)

Matryoshka Session 1


Superposition with Lambdas
Alexander Bentkamp
Joint work with Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann

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 benchmarks.


Normalizing casts inside expressions
Paul-Nicolas Madelaine

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.


Coffee break

Matryoshka Session 2


Practical higher order unification
Petar Vukmirović

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.


Superposition with Combinators
Ahmed Bhayat

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


Continued Fractions in Lean - A Newbie’s Adventure
Kevin Kappelmann

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.


Playing with booleans in a superposition prover
Visa Nummelin & Petar Vukmirović

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.


Coffee break

Matryoshka Session 4



12:00–14:00Lunch 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)

* speakers

Alexander Bentkamp (VU Amsterdam)
Jasmin Blanchette (VU Amsterdam)
Pascal Fontaine (U. Lorraine)
Hans-Jörg Schurr (U. Lorraine and Inria Nancy)
Petar Vukmirović (VU Amsterdam)

Acknowledgment: This workshop is partially supported by the ERC Starting Grant 2016 Matryoshka (grant agreement No. 713999) 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 publications.)

      This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement No. 713999.