Ettekande slaidid. [ppt]

*Abstract:* Nash equilibrium is one of the most important
solution concepts in classical game theory. However, till recently the
computational complexity of computing a Nash equilibrium in a
normal-form game was unknown. In this talk, we will give an overview
of the recent progress in this area, covering the seminal
PPAD-completeness result by Chen and Deng for 2-player normal-form
games, related results for graphical games, as well as hardness
results for several special types of Nash equilibria. The talk will be
self-contained and assumes no previous knowledge of game theory or
computational complexity.

Ettekande slaidid. [pdf]

*Abstract:* In this talk we will have a look at how the
techniques that have proven to be useful in model-based testing of
software are applicable in robotics applications. In model-based
testing the key is to model the requirements of the system, the
protocol or the behaviour of the application using some computer
readable formalism such as, for example, the protocol modelling language
Promela or a subset of your favourite programming language. The
presentation is illustrated with an experiment of model-based testing
of a robotic application using a modelling library called NModel and
Microsoft Robotics Studio.

Ettekande slaidid. [pdf]

*Abstract:* Aggressive technology scaling continues as
projected by Moore’s Law and has not shown signs of slowing down. This
provides many opportunities to achieve low-power and high-performance
computing. However, from the design point of view, experience shows
that what is possible to build in a next generation technology is
continually outpacing what is affordable to build in that
technology. And one of the true challenges in the future nanometric
designs (45 nm technologies and below) is reliability.

In this talk we are going to describe, why permanent and temporary faults are likely to have a frequency that could impair both safety-critical and even commercial applications, why, in nanometer IC technologies, the fault-free production of ICs will be close to impossible. And finally, we will introduce various methods that are devised for developing reliable and dependable systems based on not-so-dependable hardware.

Ettekande slaidid. [pdf]

*Abstract:* We prove that there are no black-box reductions
from Collision-Free Hash Functions to secure time-stamping schemes,
which means that in principle secure time-stamping schemes may exist
even if there exist no collision-resistant hash functions.We show that
there is an oracle relative to which there exist secure time-stamping
schemes but no hash function is collision-free. The oracle we use is
not new - a similar idea was already used by Simon in 1998 to show
that collision-free hash functions cannot be constructed from one-way
permutations in a black-box way. Our oracle contains a random hash
function family *f* and a universal collision-finder *A*. We
show that hash-tree time-stamping schemes that use *f* as a hash
function remain secure even in the presence of *A*. From more
practical view, our result is an implicit confirmation that
collision-finding attacks against hash functions will tell us quite
little about the security of hash-tree timestamping schemes and that
we need more dedicated research about back-dating attacks against
practical hash functions. (Joint work with Ahto Buldas.)

Ettekande slaidid. [pdf]

*Abstract:* When one looks at commitment and encryption
schemes, it is rather easy to spot the similarities between the two
cryptographic primitives. Although their functionalities are
different and they are used for different purposes, they share a
similar structure. Both encryptions and commitments make use of public
keys, but encryption schemes have an additional secret key. In both
cases the secret hiding and revealing stages occur, only the ways these
steps are handled differ. It is always possible to make a commitment
scheme from an encryption scheme. Making an encryption scheme from a
commitment scheme is trickier though, because there exists no secret
key in the simple commitment scheme construction. We look at the
properties of the two groups of schemes and show the connections
between them.

Ettekande slaidid. [ppt]

*Abstract:* Hierarchical visualisation techniques are
extensively used due to their capabilities to display the similarities
of data objects in different granularity. In our work we concentrate
on improving the visual outcome of hierarchical clustering.

For a large data set the tree with all objects cannot be presented in one picture. Therefore, collapsed nodes must be used, each giving a summarised view of the corresponding subtree. Usually, collapsing is performed on subtrees that are either at fixed depth or of fixed size. We propose an algorithm that works on data sets each object of which is described by two sets of properties. The sets are used separately at different stages of algorithm - the first set is used for hierarchical clustering whereas the other set, which consists of binary features only, is used for collapsing. The algorithm looks for subtrees with significant over-representation of some binary feature and favours these in the collapsing process.

We have built a microarray gene expression data visualisation system implementing this technique. The genes are clustered by their expression patterns using our fast approximate hierarchical clustering algorithm and Gene Ontology annotation enrichments are found using our tool g:Profiler and used to guide collapsing.

Ettekande slaidid. [pdf]

*Abstract:* To speak about the security of information flow in
programs employing cryptographic operations, definitions based on
computational indistinguishability of distributions over program
states have to be used. These definitions, as well as the
accompanying analysis tools are complex and error-prone to argue
about. Cryptographically masked flows, proposed by Askarov, Hedin and
Sabelfeld, are an abstract execution model and security definition
that attempt to abstract away the details of computational
security. The analysis of programs in this model is hopefully more
similar to the analyses for the usual forms of non-interference.

In this talk we introduce the model of cryptographically masked flows and investigate under which conditions it really is computationally sound, i.e. when does the security of a program in their model imply the computational security of this program. After spelling out a reasonable set of conditions, we will propose an even simpler model of execution that is nevertheless no more restrictive than the cryptographically masked flows together with these conditions for soundness.

*Abstract:* tba (Joint work with Yvo Desmedt and Duong Hieu
Phan.)

Ettekande slaidid. [pdf]

*Abstract:* In some applications like program slicing, it is
useful to imagine program runs as they were able to overcome
non-termination. According to this view, a computation that falls into
an infinite loop or infinitely deep recursion continues after
completing the infinite subcomputation.

Program semantics that follow this view may be called transfinite, but the word "transfinite" actually fails to characterize the whole variety of computation processes. In the case where only iterative loops can be non-terminating, the sequence of execution steps is really transfinite in the sense that the steps can be enumerated by ordinals so that their execution order corresponds to the natural order of ordinals. But in the case of infinitely deep recursion, the sequence is more like a fractal structure.

Defining such semantics even for rather simple programs with infinitely deep recursion has not succeeded so far. We show some possible definitions via greatest fixpoints of monotone operators. In order to achieve this, usual traces are replaced by either fractional traces where steps are enumerated by rational numbers from some fixed interval or trees.

Ettekande slaidid. [pdf]

*Abstract:* Circular programs are a powerful technique to
express multiple traversal algorithms as a single traversal function
in a lazy setting. In this talk, we present a shortcut deforestation
technique to calculate circular programs. The technique we propose
takes as input the composition of two functions, such that the first
builds an intermediate structure and some additional context
information which are then processed by the second one, to produce the
final result. Our transformation into circular programs achieves
intermediate structure deforestation and multiple traversal
elimination. Furthermore, the calculated programs preserve the
termination properties of the original ones. (Joint work with João
Fernandes and João Saraiva.)

Ettekande slaidid. [pdf]

*Abstract:* Partial redundancy elimination is a complex
optimization which performs common subexpression elimination and code
motion at the same time. We show that the type-systematic approach to
dataflow analyses scales up to such complicated analyses. It makes it
easy to show the soundness of optimization, but also allows proving
properties beyond soundness, such as certain optimality
results. Soundness of the optimization makes it possible to transform
a program's proof along the program guided by its analysis type
derivation. (Joint work with Tarmo Uustalu.)

Ettekande slaidid. [pdf]

*Abstract:* Visual formalisms are widely used in systems
engineering to express the requirements for the expected behaviour of
the system. Automatic Code Generators (ACG) help bridge the gap
between a visual model and the designed system's soft- or
hardware. While there exist modelling tools (e.g. Scade, Sildex,
Statemate) that are based on a sound formalism like, for example, a
synchronous language, many of the widely used tools (e.g. the
Matlab/Simulink toolset) have informally defined semantics.

A code generator for Stateflow, a Statecharts like complex visual system specification language, which is part of the widely used Matlab/Simulink toolset, is presented. The code generator is based on a refined version of the denotational semantics for Stateflow, proposed first by Hamon. The updated semantics for Stateflow and two alternative ways of code generation are presented.

Ettekande slaidid. [ppt]

*Abstract:* In bioinformatics, large graphs with genes or
proteins as vertices appear in various contexts (examples: proteins
interacting with each other, genes regulating each other). The edges
of the graph are typically obtained from biological experiments, and
different sources of data may give different sets of edges. We assign
a weight to each such dataset to indicate its trustworthiness and then
assign weights to each edge as the sum of the weights of the datasets
that contain that edge.

We are interested in finding sets of genes that are somehow biologically meaningful, such as working together to perform some action. By the function of other genes in such a set it might then be possible to guess the function of some unknown gene. For this we try to use various graph algorithms that split the graph into smaller subgraphs. Those range from simply finding connected components to more complicated clustering algorithms that find dense subgraphs, such as Markov clustering and betweenness centrality clustering.

We have developed a web-based tool for combining graph data from various sources, running different algorithms on graphs to obtain potentially meaningful subgraphs and finding the biological meaning of the subgraphs using knowledge about the function of each gene. (Joint work with Jüri Reimand and Jaak Vilo.)

Ettekande slaidid. [pdf]

*Abstract:* Designing a viable language for total (as in type
theory) functional programming is remarkably difficult: it takes a
term calculus for a type language with inductive and coinductive types
that is satisfactory both metatheoretically and practically. Basic
structured (co)recursion schemes in their standard form are not an
option, they are far too cumbersome to program with.

The alternatives include what are known as guarded and Mendler-style (co)recursion primitives. These are general-recursor like combinators. Guarded combinators are governed by syntactic side-conditions enforcing conformance of an a priori general-recursive definition to a structured (co)recursion scheme. Mendler-style combinators are cleaner: here the same effect is achieved by more restrictive typing employing universal quantification. But a problem with both is that the choice of the structured (co)recursion scheme to support is non-canonical.

We argue that one meaningful canonical solution is given by a calculus of "circular proofs", an intuitionistic propositional sequent calculus where a proof is a rational derivation tree where every path satisfies a simple progress condition. An equivalent formulation is a higher-order sequent calculus where proofs are wellfounded trees, but some inference rules are higher-order. Looked at through appropriate glasses, the calculus of circular proofs is a neat term calculus with guarded (co)recursion while the higher-order sequent calculus is a reformulation with Mendler-style (co)recursion. (Joint work with Varmo Vene.)

Ettekande slaidid. [ppt]

*Abstract:* We describe a model-based construction of an
online tester for black-box testing of the implementation under test
(IUT). The external behaviour of the IUT is modelled as an output
observable nondeterministic EFSM with the assumption that all
transition paths are feasible. A test purpose is attributed to the IUT
model by a set of Boolean variables called traps that are used to
measure the progress of the test run. These variables are associated
with the transitions of the IUT model. The situation where all traps
have been reached means that the test purpose has been achieved. We
present a way to construct a tester that at runtime selects a
suboptimal test path from trap to trap by finding the shortest path to
the next unvisited trap. The principles of reactive planning are
implemented in the form of the decision rules of selecting the
shortest paths at runtime. The decision rules are constructed in
advance from the IUT model and the test purpose. Preliminary
experimental results confirm that this method clearly outperforms
random choice and is better than the anti-ant algorithm in terms of
resultant test sequence length to achieve the test purpose. (Joint
work with Kullo Raiend, Andres Kull, Juhan Ernits.)

*Abstract:* In order to check the correctness of programs with
per-element locking schemes, we propose a new domain for
must-equalities between addresses. The domain is a smooth combination
of Herbrand and affine equalities. We present an interprocedural
algorithm that for a suitably defined core language computes all valid
equalities in polynomial time. (Joint work with Helmut Seidl and Varmo
Vene.)

Helger Lipmaa

Tarmo Uustalu

Varmo Vene

Viimane uuendus 8.10.2007