VeriDis Retreat
+

Tuesday 11 June (Room 6A04, OZW building)

Integration of Event-B and Distalgo
Alexis Grall
(abstract) (slides)

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 a CDCL(LA) Solver
Martin Bromberger
(abstract) (slides)

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
(abstract) (slides)

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.

Discussion

Wednesday 12 June (Room 7B01, OZW building)

Termination of Triangular Integer Loops is Decidable
Florian Frohn
(abstract) (slides)

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
(slides)

SCL – Clause Learning from Simple Models
Alberto Fiori

HOπ in Coq
Sergueï Lenglet
(slides)

Discussion

Encoding Challenges for Hard Problems
Marijn Heule
(abstract) (slides)

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
(abstract) (slides)

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.

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

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
(abstract) (slides)

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.

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

Extending an Isabelle Formalisation of CDCL to Optimising CDCL
Mathias Fleury
(abstract) (slides)

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
(abstract) (slides)

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é
(abstract) (slides)

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.

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

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

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
(abstract)

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.

Practical higher order unification
Petar Vukmirović
(abstract) (slides)

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
(abstract) (slides)

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)

Continued Fractions in Lean - A Newbie’s Adventure
Kevin Kappelmann
(abstract) (slides)

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ć
(abstract) (slides)

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.

Discussion