previous day
next day
all days

View: session overviewtalk overview

09:00-10:30 Session 3: Invited Talks
Temporal Logics for Multi-Agent Systems
Basic Hilbert Bases

ABSTRACT. We present an algorithm for computing Hilbert bases. A nice feature of the algorithm is that it is also a constructive proof that every basis vector of a Hilbert Basis can be written down using polynomial space, establishing that Integer Linear Programming is in NP, not only for one solution, but for all minimal basis solutions

Anti-unification for lambda-terms: a generic approach
10:30-11:00Coffee Break
11:00-12:30 Session 4: Invited Talks
Some memories from mid-late 90s and how having Andrei as my PhD advisor impacted my life

ABSTRACT. Looking back at the time when SREU was proved undecidable and how this triggered a line of followup research.

The Curse of Interpolation

ABSTRACT. Craig Interpolation is a key technique to effectiveness of SMT-based Model Checkers for infinite state systems. Starting with predicate abstraction, interpolants have been used to guess the missing terms that are required to construct an inductive invariant. In this talk, we argue that while interpolation is very effective, it is also very hard to control in practice. This leads to what we call a Curse of Interpolation -- a technique whose general success masks its inadequacy on even simple benchmarks. To mitigate the curse, we suggest an alternative approach in the context of SMT-based Model Checker Spacer.

Rewrite Encodings in Dependent Type Theories: The Problem of Confluence
12:30-14:00Lunch Break
14:00-15:30 Session 5: Invited Talks
Using Hilbert Bases for Reasoning about Multisets

ABSTRACT. In this talk we present a decidable logic for reasoning about
multisets with cardinality constraints. Such constraints naturally
arise in software verification, e.g., for programs that implement or
use container data structures. We show how to reduce reasoning about
multisets with cardinality constraints to reasoning about semilinear
sets. Using Hilbert bases we are able to solve the problem using
standard linear integer arithmetic solvers.

A Theory of Object Structures

ABSTRACT. The trickiest problems of dealing with object-oriented programs involve the object structures they produce at run time. Analyzing the precise properties of these structures, such as aliasing and null pointers (voidness), is key to program verification, compiler optimization, safe concurrency and many other applications. No existing method or tool provides a general and efficient analysis. The dual-semantics approach presented here yields a pair of sound approximations, under- and over-, of the actual object structures produced by all executions of a program. Each of these approximations provides sound answers to the corresponding properties, e.g. voidness and may-alias respectively. The method is iterative and parameterizable: since each iteration narrows the gap between the under- and over-approximations, varying the number of iterations can yield any desired level of precision. The method has been implemented, leading to efficient alias and frame analysis of object-oriented programs.

15:30-16:00Coffee Break
16:00-17:30 Session 6: Invited Talks
How to count chairs and bats in Description Logics

ABSTRACT. In recent work we have extended the expressive power of number restrictions in Description Logics by using numerical and set constraints stated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA). The resulting logic, called ALCSCC, is not a fragment of first-order logic. Using an appropriate notion of bisimulation, we are able to characterize the first-order fragment of ALCSCC in a natural way.

If you want to know how I succeed to link this topic to Andrei, you need to come to my talk.

Interpolation infusion in SMT-based model checking

ABSTRACT. This talk will present an overview of our SMT-based model checker, HighFrog, that employs interpolation techniques for program summarization and incremental safety analysis. Our interpolation engine aims at optimising verification performance and equipped with innovative solutions for generation of program abstractions flexible wrt their size and strength.

60 Shades of Grey in Vampire