Kokkuvõte: Electroactive polymers are materials that that change their shape in an electric field. Their performance resembles the performance of biological muscles and therefore they can be used as a substitute of conventional actuators and for building biomimetic devices.
However, the performance of the EAP actuators is not very well understood since their response is nonlinear and their properties vary considerably. This presentation describes preliminary tests with and underwater artificial pendulum controlled by EAP muscles.
Ettekande kiled. [pdf]
Kokkuvõte: We study binary hash functions $h\colon\{0,1\}^{2k}\rightarrow\{0,1\}^k$ for which certain (tree-shaped) computations $T^h(v_1,\ldots,v_N)$ ($v_i$ are different $k$-bit strings) are provably hard. Such functions are very useful in hash-tree applications (e.g. time-stamping, micropayments) where massive precomputations are considered as a threat.
We call a binary hash function $h$ shortcut-free iff every tree-shaped computation $T^h(v_1,\ldots,v_N)$ (in which N is sufficiently large) is hard to compute. Note that the "traditional" security properties (e.g. collision-freeness, one-wayness) do not (directly) imply shortcut-freeness. It is thereby not excluded that the results of certain (massive) hash computations can be found much easier way than direct computation.
We study the role of shortcut-freeness in the security of time-stamping schemes. We make a small step towards shortcut- free hash functions, by representing a black-box construction of a hash function for which computing the (root value of) complete Merkle tree $M_k(0,...,2^k-1)$ is provably hard. We discuss some implications of our construction to possible oracle separation results between the security properties of cryptographic hash functions.
Kokkuvõte:
Knots and Wracks - It has been known, albeit not widely, since the early sixties that the topology of a knot or link is characterized by a simple algebraic structure called a wrack. We review the basic constructions of this theory: the correspondence between link diagrams and wrack presentations, and the topological representation of a link's wrack in terms of nooses.
Data Distribution and Demi-wracks - In the early nineties Roscoe devised an algorithm for maintaining consistency when passing updates around a ring of databases. He gave an abstract correctness proof of the algorithm using an algebraic structure satisfying the wrack law. Prompted by the theory of knots and wracks, we draw the circulation of updates as links in space-time and see that the correctness of the algorithm follows directly from the topology.
Knot Theory for Computer Science - Sketch of a research programme, open questions, research directions, possible applications. Extensions of Roscoe's algorithm, other concurrent algorithms, synchronization algorithms, priority algorithms.
Ettekande kiled. [pdf]
Kokkuvõte: Eeldame, et oleme huvitatud programmide korrektsusest. Aga kuidas luua õigesti töötavaid programme? Verifitseerimise vaatenurgast vaadates on probleemi lahendamiseks vaja võtta korrektne spetsifikatsioon ning lahenduse realisatsioon ning kontrollida, kas viimane rahuldab nõudeid. Tihti on sellise lähenemise korral probleemiks spetsifikatsiooni puudumine, ebatäielikkus ja/või esitatus segases proosas, s.t. mitteformaalselt. Samas tuleb vahel ette, et programme testitakse ning kohati isegi luuakse terveid testide komplekte. Käesolev mõtiskelu püüab selgitada üht võimalust, kuidas otsida programmijooksudest etteantud mustri kohaselt välja temporaalseid omadusi ning kuidas leitud omadused võivad kasulikud olla (näiteks sama programmeerimisliidese (API) erinevate realisatsioonide võrdlemisel). Lõpuks esitame küsimuse, mida võiks anda automaatselt avastatud omaduste (spetsifikatsiooni) verifitseerimine ning kas sellest spetsifikatsioonist on mõistlik automaatselt teste genereerida?
Kokkuvõte: Ettekande esimeses osa tutvustatakse näidetele tuginedes võre kongruentsi mõistet ja mõningaid klassikalisi tulemusi võrede kongruentsivõrede ehitusest. Teises osas tõestatakse, et nn ühtlase lõpliku võre kongruentsid kommuteeruvad.
Ettekande kiled. [pdf]
Kokkuvõte: Manual "news clipping" is a time-consuming task in many EU institutions. We describe a framework for automating this procedure - a multilingual news clustering application that allows for news topic tracking by each day and over longer periods. We then describe how the news articles can be linked across languages, using a multilingual conceptual thesaurus. Finally, we explain the challenges in extending the language-dependent part of the framework to the highly inflected Estonian language and present the results. (Joint work with the JRC Language Technology group in Ispra, Italy).
Ettekande kiled. [pdf]
Kokkuvõte: Checking programs for secure information flow is an important part in building secure systems. One possible method for this task is the usage of security type systems. Checking can be done by type inference; and the fact that a program is secure can be communicated by giving the types of the program and possibly its components. In this talk we present one such type system. It is distinguished by its ability to handle cryptographic primitives, namely symmetric encryption, and to do so in a way that is correct with respect to complexity-theoretic definitions of encryption security.
Ettekande kiled. [pdf]
Kokkuvõte: Designeeritud verifitseerijaga signatuuriskeemid (DVS skeemid) erinevad tavalistest signatuuriskeemidest selle poolest, et nende autentsust saab verifitseerida vaid üks, eelnevalt designeeritud, osapool. Käesolevas artiklis murrame me lahti mitmed eelnevalt välja pakutud DVS skeemid. Osad nendest rünnetest on piisavalt uudsed selleks, et välja pakkuda uuem ja rangem turvadefinitsioon DVS skeemidele. Me pakume välja range turvadefinitsiooni DVS skeemidele. Artiklis on toodud ka uus DVS skeem, mis on tõestatavalt turvaline. Nimelt me näitame, et uue DVS skeemi turvalisus on taandatav täpse reduktsiooni abil DDH (Decisional Diffie-Hellman) probleemile mitteprogrammeeritavas juhusliku oraakli mudelis. Lisaks sellele on uus skeem efektiivsem kui mitmed eelnevalt disainitud skeemid. (koostöö Guilin Wangi ja Feng Baoga).
Kokkuvõte: The amount and distribution of underwater vegetation reflects the overall environmental condition of the whole sea region, level of pollution and climatic changes. Therefore, in Baltic Sea region, the examination of underwater vegetation is part of regular environmental monitoring. Based upon this data, important conclusions can be drawn about the environmental condition. This work is currently done by divers. Our goal is to build inexpensive small device to speed up this kind of monitoring and automatically process the video images to recognize and count different algae forms.
Ettekande kiled. [pdf]
Kokkuvõte: In "Generic Haskell", an extension of "Haskell", one can define structurally polymorphic entities: functions and datatypes that take a type argument and are defined by induction on the structure of Haskell datatypes.
Using this mechanism, functions such as equality, comparison, parsing and pretty printing, but also several forms of traversals and queries on data structures can be expressed. Such functions are defined once, in a type-safe way, and can then be used on all Haskell datatypes.
The talk introduces structural polymorphism with several examples, and gives a tour of the Generic Haskell language extension.
Ettekande kiled. [pdf]
Kokkuvõte: The general purpose of our work is to develop an underwater robot which mission is to explore and film plantation of the bottom of the sea. Problems I am dealing with are designing electronics for controlling movement of the robot. Also, appropriate sonars must be tested and installed for measuring distance between the vehicle and the bottom of the sea.
Ettekande kiled. [pdf]
Kokkuvõte: So far the use of proof carrying code has been limited to showing well-typedness of binary code, in which case the compiler automatically creates a certificate (proof) to enable efficient checking of type safety of the code. If some stronger properties are required from the binary code like adherence to an interface specification, automatic generation of proofs by the compiler becomes impossible. Instead, we need a way to transform proofs of a high level program into proofs of its compiled counterpart. Such transformations are not completely straightforward because of optimizations that typically take place during compilation. The talk will outline some of the problems that arise and discuss ways of tackling them.
Ettekande kiled. [ppt]
Kokkuvõte: Today, the most powerful method for inferring the biological function of a sequence is by similarity searching on databases. In those databases short (5 - 20bp) sequences with a common biological function are often represented in the form of matrices, as they describe better the uniform structure and increase the speed of database-queries. In my presentation I explain different weight-matrix construction methods, give an overview of most common applications and challenges.
Ettekande kiled. [pdf]
Kokkuvõte: We demonstrate that just as monads can be used as an abstraction of notions of computation with an effect, comonads can be employed to abstract notions of value in a context. We discuss two comonads whose coKleisli arrows represent general resp. causal stream functions, i.e., transformers of signals in discrete time. In particular, we discuss the application of such comonads as modularity tools for programming and for semantic description of intensional languages a la Lucid and of dataflow languages a la Lucid Synchrone, looking at simple interpreters based on comonad translations. We also discuss a representation of causal partial-stream functions, i.e., transformers of clocked signals, via a distributive law of a comonad over a monad and compare our approach to that of Freyd categories, known in functional programming as arrow types constructors. (Joint work with Varmo Vene, with contributions from Rohit Bansal.)
Ettekande kiled. [pdf]
Kokkuvõte: I will describe the computational approaches and challenges in tackling the challenging problems of understanding the gene regulation mechanisms.
Peeter Laud