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

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

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.
 

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.

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.

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.

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.