## Invited speakers

The Program Committee is delighted to announce the names of the four invited speakers:

## Per Martin-Löf

Interfering spreads and repetitive structures.

Spreads, i. e. infinite trees, are special among topological spaces by being totally disconnected, except in the extreme case when the tree consists of a single branch only. If we want to get connected spaces as well, we must allow the branches of the tree not only to diverge but also to converge. We then arrive at the notion of an interfering spread. It turns out that this notion is the same as the statistical notion of repetitive structure as formulated by Steffen Lauritzen (Danish statistician, now at Oxford) back in 1974.

Spreads, i. e. infinite trees, are special among topological spaces by being totally disconnected, except in the extreme case when the tree consists of a single branch only. If we want to get connected spaces as well, we must allow the branches of the tree not only to diverge but also to converge. We then arrive at the notion of an interfering spread. It turns out that this notion is the same as the statistical notion of repetitive structure as formulated by Steffen Lauritzen (Danish statistician, now at Oxford) back in 1974.

## Rosalie Iemhoff

(sponsored by The Danish Network for the History and Philosophy of Mathematics)

Substitutions and Rules

There are many ways to present a theory, even if just syntactic representations with axioms and rules are considered. In recent years the variety of rules that can be used to axiomatize a theory has become much better understood. And in the case of logics, a close connection between such axiomatizations and unification theory has come to light. In this talk I will give an overview of results in this area.

Substitutions and Rules

There are many ways to present a theory, even if just syntactic representations with axioms and rules are considered. In recent years the variety of rules that can be used to axiomatize a theory has become much better understood. And in the case of logics, a close connection between such axiomatizations and unification theory has come to light. In this talk I will give an overview of results in this area.

## Boban Velickovic

Towards a structure theory of Maharam algebras

A Maharam algebra is a complete Boolean algebra carrying a continuous strictly positive probability submeasure. A celeberated problem of Maharam from the 1940s asks if every such algebra is in fact a measure algebra. The problem was finally solved in 2005 by Talagrand who constructed a counterexample. We present a whole class of examples of arbitrary high exhaustivity rank and discuss some directions towards a possible structure theory of Maharam algebras.

This is joint work with Z. Perovic (San Diego)

A Maharam algebra is a complete Boolean algebra carrying a continuous strictly positive probability submeasure. A celeberated problem of Maharam from the 1940s asks if every such algebra is in fact a measure algebra. The problem was finally solved in 2005 by Talagrand who constructed a counterexample. We present a whole class of examples of arbitrary high exhaustivity rank and discuss some directions towards a possible structure theory of Maharam algebras.

This is joint work with Z. Perovic (San Diego)

## Nikolaj Bjorner

(sponsored by Microsoft “Microsoft is a trademark of the Microsoft group of companies and is used under license from Microsoft.”)

The Satisfiability Modulo Theories solver Z3 and Applications.

Modern software analysis and model-based tools are increasingly complex and multi-faceted software systems. Yet, at their core is invariably a component using logical formulas for describing states and transformations between system states. In a nutshell, symbolic logic is the calculus of computation. The state-of-the art Satisfiability Modulo Theories (SMT) solver, Z3, developed by Leonardo de Moura, Christoph Wintersteiger and the speaker at Microsoft Research, can be used to check the satisfiability of logical formulas over one or more theories. SMT solvers offer a compelling match for software tools, since several common software constructs map directly into supported theories. Many central problems in program analysis and verification are also slightly disguised SMT problems, such as synthesizing inductive invariants as satisfiability of recursive Horn clauses. We describe the algorithmic underpinnings for solving such SMT problems, and also several of the applications where Z3 is used, including the Windows 7 static driver verifier, the SAGE white-box fuzzer and for checking security policies.

The Satisfiability Modulo Theories solver Z3 and Applications.

Modern software analysis and model-based tools are increasingly complex and multi-faceted software systems. Yet, at their core is invariably a component using logical formulas for describing states and transformations between system states. In a nutshell, symbolic logic is the calculus of computation. The state-of-the art Satisfiability Modulo Theories (SMT) solver, Z3, developed by Leonardo de Moura, Christoph Wintersteiger and the speaker at Microsoft Research, can be used to check the satisfiability of logical formulas over one or more theories. SMT solvers offer a compelling match for software tools, since several common software constructs map directly into supported theories. Many central problems in program analysis and verification are also slightly disguised SMT problems, such as synthesizing inductive invariants as satisfiability of recursive Horn clauses. We describe the algorithmic underpinnings for solving such SMT problems, and also several of the applications where Z3 is used, including the Windows 7 static driver verifier, the SAGE white-box fuzzer and for checking security policies.