LICS 2008 - Invited Speakers

Abstracts of Invited Talks

David Basin, ETH Zurich
Title: Cryptographically Sound Protocol-Model Abstractions

We present a formal theory for cryptographically-sound theorem proving. Our starting point is the Backes-Pfitzmann-Waidner (BPW) model, which is a symbolic protocol model that is cryptographically sound in the sense of blackbox reactive simulatability/UC. To achieve cryptographic soundness, this model is substantially more complex than standard symbolic models and the main challenge in formalizing and using this model is overcoming this complexity. We present a series of models that successively abstract the original BPW model, bringing it closer to standard Dolev-Yao style models, while preserving cryptographic soundness. As our models are state-based, we have also developed monad-based tools for formalizing and reasoning about these models. We present a case study showing that our abstractions and tools enable proofs of complexity comparable to those based on more standard models. Our entire development has been formalized in Isabelle/HOL.

Martin Grohe, Humboldt University Berlin
Title: The Quest for a Logic Capturing PTIME

The question of whether there is a logic that captures polynomial time is the central open problem in descriptive complexity theory. It was first asked by Chandra and Harel (1982) in the context of database theory, and later in a slightly different form by Gurevich (1988) in the context of finite model theory. Essentially, a logic captures PTIME if the properties of finite structures definable in the logic are precisely those decidable in polynomial time. (But there are subtleties in the definition of what constitutes a logic in this context.)
In this talk, I will review the question and the early, mostly negative results that were obtained until the mid 1990s. I will then turn to positive results showing that fixed-point logic with counting captures PTIME on several interesting classes of structures, among them planar graphs and graphs of bounded tree width. This part of the talk will include recent results on definability in fixed-point logic and graph structure theory. Finally, I will dicuss stronger logics formed by adding algebraic operators to fixed-point logic, and I will propose some open problems and directions for further research.

Dexter Kozen, Cornell University
Title: Nonlocal Flow of Control and Kleene Algebra with Tests

Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA), or the algebra of regular expressions, with Boolean algebra. It can model basic programming and verification constructs such as conditional tests, while loops, and Hoare triples, thus providing a relatively simple equational approach to program equivalence and partial correctness. In this paper we show how KAT can be used to give a rigorous equational treatment of control constructs involving nonlocal transfer of control such as gotos, loop statements with multi-level breaks, and exception handlers. We develop a compositional semantics and an equational axiomatization. The approach has some novel technical features, including a treatment of multi-level break statements that is reminiscent of de Bruijn indices in the variable-free lambda calculus. We illustrate the use of the system by giving a purely calculational proof that every deterministic flowchart program is equivalent to a loop program with multi-level breaks.

Yiannis Moschovakis, UCLA and University of Athens
Title: The Axiomatic Derivation of Absolute Lower Bounds

The ancient Euclidean algorithm computes the greatest common divisor gcd(m,n) of two natural numbers from (or relative to) the remainder operation, rem, which is assumed as primitive; it requires no more than 2 log(min(m,n)) applications of the remainder operation to compute gcd(m,n) (for m,n >= 2), and it is not known to be optimal:
Conjecture. For every algorithm A which computes on N from rem the greatest common divisor function, there is a constant r>0 such that for infinitely many pairs a>=b>=1, c_A(a,b) >= r log_2(a),
where c_A(m,n) counts the number of calls to ``the remainder oracle'' required by α for the computation of gcd(m,n). The conjecture claims a logarithmic lower bound for all algorithms which compute gcd(m,n) from the remainder operation, not just those expressed by a specific class of computation models.
In this lecture I will develop an approach to the theory of algorithms in the style of abstract model theory which makes it possible to make precise and (on occasion) prove the existence of non-trivial, absolute lower bounds for a wide variety of problems and specified primitives.

Back to the LICS 2008 web page.