Invited Talks

Kim Larsen

Aalborg Universitet, Denmark
Tuesday 6 April, 16:00
Verifying LEGO: Validation and Synthesis of Embedded Software
Embedded systems are to be found almost everywhere in todays society. Intelligence in form of software and hardware is introduced into all kinds of products and sectors with the objective of enhancing their functionality. Examples include consumer electronics (e.g. MP3 players, audio/video systems), transport systems (e.g. ABS in cars, control software in high speed trains), medical devices (intelligent pens for treating diabetis), and many others.

As indicated by the examples above, embedded software are often applied in highly safety cricial applications. The increased complexity of embedded systems challenges the methods used for designing and realising embedded systems, in order that they are bug-free, correct, predicatable and fault-tolerant. In addition, embedded systems are often used in situation where timing garantees (e.g. the release of an airbag in a car must happen within a few millisecond after impact regardsless) as well as bounds on usages of resorces (memory, power, bandwidth) are crucial properties making this effort even more difficult.

In the talk we will introduce the real-time validation tool UPPAAL (www.uppaal.com) and demonstrate on a number of embedded system examples realized in LEGO Mindstorm how UPPAAL enables to find and correct bugs as well as optimize resource consumption.

Gil Kalai גיל קלעי

Hebrew University of Jerusalem, Israel האוניברסיטה העברית בירושלים
Wednesday 7 April, 09:00
Analysis and Probability of Boolean Functions
Boolean functions (under various names) are important in combinatorics, probability theory, computer science, game theory, and other areas. In the talk I will discuss a few results and some problems concerning analysis and probability of Boolean functions. In the (self-contained and friendly for students) lecture I will describe first a few notions:
  1. Influence: The definition and properties of the influence of a variable on a Boolean function. (Related to: the power of a voter for an election rule; the effect of malicious processors in a collective coin flipping.)
  2. Noise-sensitivity: How sensitive is a Boolean function to noise? (Related to how likely it is that errors in counting the votes will change the outcomes of an election.)
  3. The Fourier Walsh expansion
Next I will briefly describe a few results: the existence of influential variable (KKL), the tradeoff between total influence and noise sensitivity (BKS) and the majority is stablest (MOO).

Next two conjectures will be presented the first on the relation between expectation threshold and the actual threshold (with Jeff Kahn) and the wsecond about the noise stability conjecture for monotone threshold circuits and the reverse Boppana-Håstad conjecture (with Itai Benjamini and Oded Schramm).

Finally two extensions will be mentioned: (a) Maps from Σn to Σ where Σ is a larger alphabet and their thresholds (with Elchanan Mossel), and (b) maps from {0,1}mn to {0,1}m in the context of judgement aggregation (with Muli Safra and Moshe Tennenholtz).

Catuscia Palamidessi

INRIA-Saclay and École Polytechnique, France
Wednesday 7 April, 14:00
Information-Theoretic approaches to Information Flow
In recent years, there has been a growing interest in considering the quantitative aspects of Information Flow, partly because often the a priori knowledge of the secret information can be represented by a probability distribution, and partly because the mechanisms to protect the information may use randomization to obfuscate the relation between the secrets and the observables. Among the quantitative approaches to Information Flow, the most prominent is the one based on Information Theory, which interprets a system producing information leakage as a (noisy) channel between the secrets (input) and the observables (output), and the leakage itself as the difference between the Shannon entropies of the input before and after the output (Mutual Information). This approach however suffers from two shortcomings:
  1. The Shannon entropy is not the most suitable measure in case of the typical attacks in security (in particular, the one-try attacks), and
  2. the analogy with the (simple) channel collapses in case of an interactive system.
In this talk we discuss these issues and propose some solutions.

Ulrike Sattler

University of Manchester, U.K.
Thursday 8 April, 09:00
Automated Reasoning for Ontology Engineering
In the last decade, "ontologies" are being developed as logical theories capturing domain knowledge, and used in a variety of applications, most prominently in clinical and life sciences. They are used to design and maintain terminologies, to base information systems on, and to provide flexible access to data. Description Logics, i.e., decidable fragments of first order logic, are used as the basis for ontology languages such as OWL, and the standardisation of these ontology languages has led to an increasing number of applications and tool developments, and to an increased interest in automated reasoning services.

I will briefly introduce OWL and describe its relationship with other logics, and then describe some of the recent developments in automated reasoning for ontology engineering. On the one hand, progress was made regarding standard reasoning tasks: e.g., we have seen the development of new reasoning techniques to cope with extremely large, modestly complex theories and to answer queries against databases w.r.t. ontologies. On the other hand, the "serious" usage of ontologies requires ever more and powerful non-standard reasoning services such as the extraction of modules or the explanation of entailments from an ontology.

I will assume a basic knowledge of first order or modal logic, and hope to provide an interesting overview of this lively area of logic- based knowledge representation.

Erik Demaine

Massachusetts Institute of Technology, U.S.A.
Thursday 8 April, 14:00
Algorithms Meet Art, Puzzles, and Magic
When I was six years old, my father Martin Demaine and I designed and made puzzles as the Erik and Dad Puzzle Company, which distributed to toy stores across Canada. So began our journey into the interactions between algorithms and the arts (here, puzzle design). More and more, we find that our mathematical research and artistic projects converge, with the artistic side inspiring the mathematical side and vice versa. Mathematics itself is an art form, and through other media such as sculpture, puzzles, and magic, the beauty of mathematics can be brought to a wider audience. These artistic endeavors also provide us with deeper insights into the underlying mathematics, by providing physical realizations of objects under consideration, by pointing to interesting special cases and directions to explore, and by suggesting new problems to solve (such as the metapuzzle of how to solve a puzzle). This talk will give several examples in each category, from how our first font design led to a universality result in hinged dissections, to how studying curved creases in origami led to sculptures at MoMA. The audience will be expected to participate in some live magic demonstrations.

Johan Håstad

Kungliga Tekniska Högskolan, Sweden.
Friday 9 April, 09:30
Approximation Resistance
Consider 3Sat, the problem of satisfying a number of clauses each being the disjunction of exactly three literals. It is one of the basic NP-complete problems. It has a maximization companion Max-3-Sat which asks to satisfy as many clauses as possible.

Max-3-Sat is easily seen to be NP-hard to solve exactly but turns out to remain NP-hard in much weaker, approximate, forms. Given a satisfiable instance with m clauses and ε>0, it is NP-hard to find an assignment that satisfies (7/8+ε)m clauses. As a random assignment satisfies 7m/8 clauses this result can be interpreted as saying that efficient computation cannot do anything useful for Max-3-Sat.

We say that a predicate P is "approximation resistant" if, for the problem above with the predicate P taking the role of "disjunction of three literals", it is computationally hard to find an assignment that does better than a random assignment even when (almost) all constraints can be satisfied simultaneously.

We will survey many of the results relating to approximation resistance giving both positive and negative results as well as some indication of the proof-techniques involved.