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.)