Gordon Pace: Model checking hardware compilers

Ettekande slaidid. [pdf]

Abstract: The use of hardware compilers to generate complex circuits from a high-level description is becoming more and more prevalent in a variety of application areas. However, this introduces further risks as the compilation process may introduce errors in otherwise correct high-level descriptions of circuits. In this talk, I will be presenting techniques to enable the automatic verification of hardware compilers through the use of finite-state model checkers and their application on a simple regular expression hardware compiler. It will be followed by a discussion on how these techniques can be further developed and used on more complex hardware-description languages. (Joint work with Koen Claessen.)

Juhan Ernits: Optimal scheduling using model checking

Ettekande slaidid. [pdf]

Abstract: The talk explains how scheduling can be done using model checking. The main emphasis is on using Spin for solving scheduling problems, explaining how the problems can be formulated in Promela and how the search space can be pruned. We will also have a look at whether the method can be further enhanced with iterated search refinement that utilises bitstate hashing.

Pavel Grigorenko: Attribute semantics of declarative languages

Ettekande slaidid. [pdf]

Abstract:Some extensions of attribute models and an efficient method of dynamic evaluation of attributes make them a convenient instrument for implementation of a wide class of declarative languages. In the present talk we introduce higher-order attribute models that include more control information than conventional ones. Three kinds of attribute semantics of declarative languages, and in particular, of visual languages with graph structure of sentences are described. An algorithm for dynamic evaluation of attributes is explained that is in essence the algorithm of structural synthesis of programs.

Jevgeni Kabanov: Aranea - a web framework construction and integration kit

Artikkel. [pdf]

Ettekande slaidid. [ppt]

Abstract: Currently there exist dozens of web controller frameworks that are incompatible, but at the same time have large portions of overlapping functionality that is implemented over and over again. Web programmers are facing limitations on code reuse, application and framework integration, extensibility, expressiveness of programming model and productivity.

In this paper we propose a minimalistic component model Aranea that is aimed at constructing and integrating serverside web controller frameworks in Java. It allows assembling most of available web programming models out of reusable components and patterns. We also show how to integrate different existing frameworks using Aranea as a common protocol. In its default configuration Aranea supports both developing sophisticated user interfaces using stateful components and nested processes as well as high-performance stateless components.

We propose to use this model as a platform for framework development, integration and research. This would allow combining different ideas and avoid reimplementing the same features repeatedly. An open source implementation of Aranea framework together with reusable controls, such as input forms and data lists, and a rendering engine are ready for real-life applications. (Joint work with Oleg Mürk, presented at PPPJ 2006.)

Peeter Laud: Using data flow analysis for automatic checking of computational confidentiality in cryptographic protocols

Ettekande slaidid. [pdf]

Abstract: We present a data flow analysis for cryptographic protocols using the Backes-Pfitzmann-Waidner universally composable cryptographic library. The results of the analysis can be used to easily check whether the protocol satisfies the notions of payload secrecy or key secrecy. Payload secrecy means that the protocol does not help leaking to the adversary the secrets handed to the protocol (although they may leak through means not under the control of the protocol). Key secrecy means that the newly generated and exchanged key for symmetric encryption may be used as a secret key in any application between the parties that exchanged it.

Our result is the first fully automatic analysis method for protocols using the abovementioned cryptographic library. As the method is not that different from methods used in the Dolev-Yao model, we believe that most of the extensive work done there carries over to our model. (Joint work with Michael Backes.)

Sven Laur: Kaks vaatepunkti krüptograafilistele reduktsioonidele

Ettekande slaidid (lühendatud). [pdf]

Abstract: Ettekandes käsitleme mõningaid lihtsamaid teadmushõive (knowledge-extraction) tehnikaid ning tutvustame neile vastavaid uusi tulemusi. Täpsemalt on ettekande tulipunktis küsimused: Kas musta kasti reduktsioonid on turvalisemad kui valge-kasti reduktsioonid? Kas üldse leidub praktilisi valge-kasti (white-box) reduktsioone? Osutub, et teoreetilistest piirangutest hoolimata saab teha konstruktiivseid valge-kasti reduktsioone ning esimesel küsimusel on kaks vastust sõltuvalt sellest, kas teoreetiliseks lähtepunktiks on klassikaline statistika või Bayesi statistika.

Helger Lipmaa: Lühikesed sertifikaadid NP-keeltele ekstraheeritavate algoritmide eeldusel

Abstract: Konstrueerime väikese suhtlusega interaktiivse kaheteatelise argumendisüsteemi suvalise NP-keele jaoks. Turvatõestuseks toome sisse uue keerukusteoreetilise eelduse, mis pakub iseseisvat huvi keerukusteoreetikutele.

Härmel Nestra: On duality in functional programming

Ettekande slaidid. [pdf]

Abstract: Duality is a phenomenon widely occurring in the real world and all kinds of artificial worlds like programming languages. We seek potential new dual constructs in functional programming languages.

Leopold Parts: Statistics and comparative sequence analysis

Ettekande slaidid. [pdf]

Abstract: Comparative sequence analysis is a powerful method of determining functional regions in genomes, but getting genomic data is expensive. In our talk, we will review a model for determining a combination of genomes to sequence, and discuss aspects of machine learning approaches used in classifying regions of conservation based on the work on the fly genome.

Jaan Penjam: Revisiting wreath products of automata

Ettekande slaidid. [pdf]

Abstract: We recall attributed automata as a means for software specification. Taking a categorical approach, we discuss the decomposition methods for automata using the concept of wreath products. Wreath products can be understood as a very general decomposition operation of which the various flavours of serial and parallel compositions are instances.

Jaan Penjam: 65 years from the birth of Uno Kaljulaid

Ettekande slaidid. [pdf]

Abstract: On October 21 this year, a teacher of many Estonian mathematicians and computer scientists, Uno Kaljulaid, would have turned 65. He had an interesting personality. As a mathematician, he was much influenced by Yu. Manin and B. Plotkin, however, both of them claim that they have not been his teachers. B. Plotkin was officially the supervisor of Uno’s Candidate thesis but took Uno as a colleague and not as a student. The list of students officially supervised by Uno Kaljulaid is not very long, but there are many people who say, "Uno gave me so much, I feel myself as his student!"

Something similar happened to his scientific heritage. Against today's criteria, the list of his publications is not long. But he was recognised by worldwide publishing companies and Zentralblatt Math. as a valuable reviewer. He was a dedicated mathematician with a broad erudition. He prepared good research plans and was always working hard, but being exacting in everything he did, he always had something to polish and seldom finished his papers. He left behind a remarkable number of manuscripts; many of them have not lost actuality and are worth finishing by his descendants.

The most prominent research result of Uno Kaljulaid was his Candidate thesis, defended in Minsk in 1979. This thesis was devoted to representation theory in the spirit of his advisor B. Plotkin: representations of semigroups and algebras, especially extensions to this situation, and applications of the notion of triangular product of representations for groups introduced by Plotkin. Through representation theory, Uno also became interested in automata theory, which at a later phase became his main area of interest. Another field of research concerns combinatorics. Uno Kaljulaid was also very much interested in the history of mathematics. In particular, he took vivid interest in the life and work of the remarkable 19th century Dorpat (Tartu) algebraist Th. Molien. Uno was also very interested in teaching and exposition and in popularization of mathematics.

I would like to share my memories and give some insights into Uno Kaljulaid’s life and activities.

Hedi Peterson: Discovery of regulatory motifs in Saccharomyces cerevisiae as a first step of understanding the gene regulation of baker's yeast

Ettekande slaidid. [pdf]

Abstract: One third of predicted open reading frames in S. cerevisiae are either functionally or regulatorily uncharacterized. Using Gene Ontology (GO) dataset we can identify functionally related groups of genes and discover regulatory motifs for those groups. We have identified several new motifs for a number of GO groups. Most of the strong motifs can also be discovered from seven orthologous yeasts, suggesting the motifs are evolutionary conserved and therefore supporting the importance of the discovered motifs.

We show that incorporating newly found GO specific motifs with protein-protein interactions enables to expand functionally related gene groups with new members sharing the possible regulators. Using this approach we are able to annotate a number of uncharacterized genes to GO groups and specify the functional annotations for previously known genes.

Jüri Reimand: GOSH - a gene ontology statistics mining tool

Ettekande slaidid. [ppt]

Abstract: High throughput technologies such as microarray experiments often produce large groups of potentially interesting genes that are hard to analyze by hand. The genes may have similar expression profiles under certain experimental conditions, form a subgraph in a putative protein interaction network or share a common regulatory motif, for example. Even though little may be known about a group of genes in general, large amounts of data can be found about the specific genes of a given group. One frequently used data source is the Gene Ontology (GO), which contains thousands of hierarchically related terms of biological processes, cellular components and molecular functions. Genes from many genomes have been annotated to the terms of the GO. These GO annotations of individual genes have been shown to be valuable in estimating the common properties of the whole group. For example, the fact that a statistically significant subset of a group of genes is known to be involved in a certain biological process like ribosome biogenesis, for example, may aid in hypothesizing about the function of previously unknown genes that also appear in the same group of genes.

An approach commonly used in GO tools involves determining those GO terms that significantly overlap the query set. We have studied the choice of statistical significance thresholds both empirically via randmization experiments, as well as analytically, taking into account the numbers and sizes of various GO association sets in order to avoid the problems caused by multiple testing. We also propose methods that allow to use the hierarchical structure of the GO to provide users with more condense and structured representation of the results. Second, we study the case where the genes inside the group may be ranked according to some important measure. For example, we may create an ordered list of genes by sorting genes based on the measure of the differential expression, or simply based on the co-expression similarity from a specific gene of interest. We propose a method that analyses such ordered lists of genes incrementally and demonstrate the visualization and interpretation of such data.

The methods have been implemented with a graphical public web interface, as well as a set of programs suitable for large-scale analysis on computer farms and computational GRIDs.

Ando Saabas: A Java bytecode editor

Ettekande slaidid. [pdf]

Abstract: Java bytecode is the intermediate representation of Java programs. Understanding it is crucial if one wants to develop a compiler, a bytecode verifier or an optimizer, or do low level debugging or performance/memory usage tuning. For these tasks, it is also important to have a suitable bytecode viewer and editor.

In my talk, I give a brief overview of the Java bytecode language and the inner workings of the Java virtual machine, and also demonstrate a bytecode editor that I have built on top of the jclasslib bytecode viewer.

Maarika Traat: A step towards natural-sounding speech generation

Ettekande slaidid. [pdf]

Abstract: In recent years considerable advances have been made in speech generation. However, the speech still does not sound very natural. One of the main problems is the lack or the misuse of intonation (speech melody): the computer generated speech either sounds completely monotonous, or if some heuristic method is used to determine the intonational peaks, the accents often do not fall onto the appropriate words.

People use intonation in a purposeful manner: for example, to mark new information or to highlight contrastive information. Thus information structure (the way people package the informational content in their sentences) and intonation are strongly connected.

If we treat information structure as an aspect of meaning, it would make sense to incorporate it in the semantics that is used as the input to context-to-speech generation. In this talk I present an approach of incorporating information structure in a semantic formalism (Discourse Representation Theory), and then further embedding the semantics in a grammar formalism (Unification-Based Combinatory Categorial Grammar). This framework is suitable for analysing intonationally annotated text to infer the underlying information structure, as well as for generating intonationally annotated text from a semantic representation that is marked with information structure.

Ilja Tšahhirov: Control and data dependency-based automated analysis of security protocols for confidentiality

Ettekande slaidid. [pdf]

Abstract: We present a graph-based technique being developed for specifying the protocols as a set of operations and data and control dependencies between them. The confidentiality of the protocol is defined based on a certain games driven by the adversary. Security of the protocol is analysed based on data and control dependency model, with graph transformations made based on the properties of the cryptographic primitives. The technique is the development on authors' earlier works in this area. (Joint work with Peeter Laud.)

Tarmo Uustalu: Foundational certification of data-flow analyses

Ettekande slaidid. [pdf]

Abstract: Laud et al. have demonstrated that classical data-flow analyses, such as live variables analysis, available expressions analysis etc., are usefully specifiable as type systems. These are sound and, in the case of distributive analysis frameworks, complete wrt. appropriate natural semantics on abstract properties (the underlying abstract interpretations). Applications include certification of analyses and "optimization" of Hoare triple derivations alongside programs. On the example of live variables analysis, we show that analysis type systems are applied versions of more foundational Hoare logics describing either the same property semantics as the type system or a more basic natural semantics on transition traces of a suitable kind. The rules of a type system are derivable in the Hoare logic for the abstract property semantics and those in turn in the Hoare logic for the transition trace semantics. This reduction of the burden of trusting the certification vehicle can be compared to foundational proof-carrying code, where general-purpose program logics are preferred to special-purpose type systems and universal logic to program logics. A more practical application of the foundational formalisms is certification of data-dependent analyses. (Joint work with Maria João Frade and Ando Saabas.)

Varmo Vene: Parametricity and strong dinaturality

Ettekande slaidid. [pdf]

Abstract: We recall the categorical notions of dinaturality and strong dinaturality and show that they are useful tools for reasoning about theories such as system F which contain both impredicative quantification and mixed-variant types. While it is known that models of system F which are sound for logical relations are also sound for dinaturality, the same is not the case for strong dinaturality. However we show that logical relations can be used to show that certain terms are strongly dinatural - pleasingly all the instances of terms we require for our applications turn out to be covered. (Joint work with Neil Ghani, Patricia Johann and Tarmo Uustalu.)

Jan Willemson: On the Gordon and Loeb model for information security investment

Ettekande slaidid. [pdf]

Abstract: In this presentation we discuss a simple and general model for evaluating optimal investment level in information security proposed by Gordon and Loeb in 2002. The authors leave an open question, whether there exists some universal upper limit for the level of optimal security investments compared to the total cost of the protected information set. They also conjecture that if such a level exists, it could be 1/e ~ 36.8%. In this paper, we disprove this conjecture by constructing an example where the required investment level of up to 50% can be necessary. By relaxing the original requirements of Gordon and Loeb just a little bit, we are also able to show that within their general framework examples achieving levels arbitrarily close to 100% exist. (Presented at WEIS 2006.)

Peeter Laud
Helger Lipmaa
Tarmo Uustalu
Varmo Vene
Viimane uuendus 5.10.2006