Slides from the talk [pptx]

*Abstract:* In this paper we address the problem of diagnosing
behavioral differences between pairs of business process models. The
proposed solution is based on a translation from process models to
Asymmetric Event Structures (AES). An AES represents the behavior of
a process by means of events and binary behavioral relations. So, in
order to find a behavioral representation (AES) of a process model
that represents the behavior in a more succinct manner, we propose a
technique to reduce the AES while preserving canonicity. Moreover,
the AES of a process model with cycles is infinite and, therefore, we
propose a notion of unfolding that captures all possible causes of
each process's task. From there we derive an AES where repeated events
are distinguished from non-repeated ones and that allows us to
diagnose differences in terms of repetition and causal relations in
one model but not in the other.

Joint work with Paolo Baldan, Marlon Dumas, Luciano García-Bañuelos, presented at BPM 2014.

Slides from the talk [pdf]

*Abstract:* Localized widening and narrowing, as proposed
Amato and Scozzari, is an interesting improvement of the classical
widening and narrowing approach. In many cases, it is able to improve
precision of the analysis automatically---without changing the
analysis domain. However, it is unable to cope with local solving and
non-monotonic transfer functions.

In some aspects, the work of Amato and Scozzari is similar to the work of Apinis, Seidl and Vojdani, who considered non-monotonicity and local solving. Together, we now show how the effects of localized widening and narrowing can be achieved in a generic framework with local solving.

Slides from the talk [pdf]

*Abstract:* In his 1966 paper, P. Martin-Löf addressed the
question: what does it mean for a single sequence (rather than a
distribution of) to be random? His answer formalizes the intuitive
idea that a random object should not display any "recognizable"
regularities. Later, P. Hertling and K. Weihrauch expanded this notion
to define randomness for objects of more general classes, such as
*d*-dimensional configurations, of which bi-infinite sequences
are a special case.

Cellular automata (briefly, CA) are models of synchronous parallel
computation, where the next state of each node of a regular grid
(e.g., the Cayley graph of a group) is a function of the current state
of a finite neighborhood of the node itself, different nodes having
neighborhoods of identical shape. Several noteworthy facts about CA
are known, among those: the 2001 result by C. Calude et al. that the
global function of a *d*-dimensional CA is surjective if and only
if it preserves Martin-Löf randomness of configurations; and the 2010
result by L. Bartholdi that preservation of the product measure
(generated by setting *1/K^N* as the measure of the set of the
configurations on *K* states taking given values on *N*
given points) of surjective CA characterizes amenable groups, a class
introduced by J. von Neumann to explain the Banach-Tarski paradox.

This talk, which is a continuation of the one I gave at the Estonian-Latvian Theory Days in Medzabaki, is divided into two parts. In the first one, we illustrate the Hertling-Weihrauch procedure in the specific case of configurations over finitely generated groups with decidable word problem. In the second part, we discuss our 2013 result with P. Guillon (CNRS and IML Marseille) and J. Kari (University of Turku) that, for this class of groups, Calude's property is equivalent to amenability: in particular, we show that on every non-amenable, finitely generated group with decidable word problem there exists a CA such that every Martin-Löf random configuration has a nonrandom image and only nonrandom preimages.

*Abstract:* We describe a basic framework for incremental
computing in Haskell and develop a notion of change and change
application for sequences. Finally, we implement an efficient
algorithm for incremental stable sorting of sequences.

Joint work with Wolfgang Jeltsch.

Slides from the talk [pdf]

*Abstract:* Secure multi-party computation platforms are
becoming more and more practical. This has paved the way for
privacy-preserving statistical analysis using secure multi-party
computation. Simple statistical analysis functions have been emerging
here and there in literature, but no comprehensive system has been
compiled. We consider the most used statistical analysis functions in
the privacy-preserving setting including simple statistics, t-test,
chi-square test, Wilcoxon tests and linear regression. We introduce a
privacy-preserving statistical analysis tool called Rmind that works
on the Sharemind platform and is similar to the statistics environment
R that is widely used among data analysts. This tool allows analysts
to perform statistical queries on Sharemind databases without
requiring them to have a thorough background in cryptography.

Slides from the talk [pdf]

*Abstract:* Secure multiparty computation (SMC) platforms like
Sharemind are provided with an application programming language that
abstracts away from underlying cryptography. The language does not
abstract away from one detail - the SMC protocols do not hide the
execution trace of the program, hence one cannot branch on private
values. One can only perform the computations in both branches and
obliviously merge them afterwards; this transformation is supported on
some platforms. Hence the application performs many operations, the
result of which is afterwards discarded.

In this talk we present an optimization that looks for common functionality in different branches and tries to merge them together, thereby reducing the total number of operations the application has to perform.

Joint work with Alisa Pankova.

Slides from the talk [pdf]

*Abstract:* The Internet has become part of our critical
communication infrastructure and has revolutionised the lives of many
people. However, security in cyberspace is still an underdeveloped
field. This is partially due to the fact that the Internet was
developed without a clear security concept in mind and also partially
due to the fact that it is lucrative now for criminals to find security
holes. Overall, cyber security is a critical skill for everyone using
the Internet.

We start this talk by improving cyber security training courses. Practical hands-on training courses have proven very valuable in teaching basic concepts, but it?s hard to setup and prepare high-quality courses. Among the problems is that each lab needs a realistic environment, configured with a magnitude of services and consisting of complex network technology. To recognise the true value of such labs, we need to reduce the complexity of building, configuring, deploying and monitoring those emulated networks.

We argue that this can be achieved by translation from a high-level network design into a concrete set of router and service configurations that automatically deploy onto several emulation platforms. We will then continue to show that such a system is not only be beneficial for teaching cyber security, but can also be used as a large-scale security evaluation platform that studies novel technology in the context of a realistic network environment. We conclude by outlining how such a high-level configuration framework may change how networks are configured in the future and thus lead towards an Internet design that has a security concept in mind.

Slides from the talk [pdf]

*Abstract:* We present a generic method for turning passively
secure protocols into protocols secure against covert attacks. We use
beaver triples to make it possible to verify a protocol execution by
running it locally on shares. The method adds a longer preprocessing
phase and a short post-execution verification phase to the protocol
that allows a misbehaving party to escape detection only with
negligible probability. The execution phase, after which the computed
protocol result is already available for parties, has only negligible
overhead added by our method. We present our result for three parties,
but it should be possible to extend it to any number of
parties. Differently from our previous results, the verification can
be easily adjusted to computation on rings, not only on fields, and
hence it can be more easily applied to existing secure multiparty
computation platforms.

Joint work with Peeter Laud.

Slides from the talk [pdf]

*Abstract:* Two of the major branches in secure multi-party
computation research are secret sharing and garbled circuits. This
work succeeds in combining these to enable seamlessly switching to the
technique more efficient for the required functionality. As an
example, we add garbled circuits based IEEE 754 floating-point numbers
to a secret sharing environment achieving very high efficiency and the
first, to our knowledge, fully IEEE 754 compliant secure
floating-point implementation.

Joint work with Pille Pullonen.

*Abstract:* I'll give an overview of the sightsmap.com
project, in particular the dimensions of place popularity and the
tagging algorithms using photo titles as input. I'll also give a
brief overview about the related analysis methods using mobile
positioning.

*Abstract:* We present a quantum position verification scheme
in the random oracle model. In contrast to prior work, our scheme does
not require bounded storage/retrieval/entanglement assumptions. We
also give an efficient position-based authentication protocol. This
enables secret and authenticated communication with an entity that is
only identified by its position in space.

Presented at CRYPTO 2014.

Slides from the talk [pdf]

*Abstract:* What structure is required of a set so that
computations in a given notion of computation can be run statefully
with this set as the state space? Some answers: To be able to serve
stateful computations, a set must carry the structure of a lens; for
running interactive I/O computations statefully, a
"responder-listener" structure is necessary etc. I will observe that,
in general, to be a runner of computations for an algebraic theory
(defined as a set equipped with a monad morphism between the
corresponding monad and the state monad for this set) is the same as
to be a comodel of this theory, ie a coalgebra of the corresponding
comonad. I will work out a number of instances. I will also compare
runners to handlers.

Slides from the talk [pdf]

*Abstract:* Automated software testing is an increasing trend
for improving the productivity and quality of software development
processes. That, in turn, rises issues of trustability and
conclusiveness of automatically generated tests and testing
procedures. The main contribution of this paper is the methodology
and tools of proving the correctness of tests for remote testing of
systems with time constraints. To demonstrate the feasibility of the
approach we show how the abstract conformance tests are generated,
verified and made practically executable on distributed model-based
testing platform dTron.

*Abstract:* In this talk I will highlight some connections
between the physics of magnets, artificial neural networks, and brains
that have contributed to a better understanding of complex phenomena
in each of them.

Slides from the talk [pdf]

*Abstract:* We present and compare two different
implementations of quotient types in Intensional Type Theory. We first
introduce quotients as particular inductive types following the
extension of Calculus of Constructions with quotient types from Martin
Hofmann's 2005 PhD thesis. Then we give an impredicative encoding of
quotients. This implementation is reminiscent of Church numerals and
more generally of encodings of inductive types in Calculus of
Constructions.

*Abstract:* I describe some recent progress in our research
into static analysis of embedded controllers in the automotive
domain. We previously described how standard analysis techniques can
be applied to interrupt-driven priority scheduling [POPL '11]. We were
extremely happy until our project partners evaluated our analysis in
their industrial use cases. As it happens, despite the wonderful set
of synchronization mechanisms provided by the priority-scheduled
operating system, programmers often used their own hand-written
synchronization idioms. Instead of acquiring locks, they rely on
programming logic and the state of program variables to ensure
mutually exclusive access to shared data. In order to cope, we present
a method to analyze programs using value-dependent synchronization
[VMCAI '14].

Joint work with Martin Schwarz, Helmut Seidl and Kalmer Apinis.

Helger Lipmaa

Tarmo Uustalu

Varmo Vene

Viimane uuendus 20.2.2015