ABSTRACT. In this tutorial, I will present SEAHORN, a software verification framework. The key distinguishing feature of SEAHORN is its modular design that separates the concerns of the syntax of the programming language, its operational semantics, and the verification semantics. SEAHORN encompasses several novelties: it (

1. encodes verification conditions using an efficient yet precise inter-procedural technique,
2. provides flexibility in the verification semantics to allow different levels of precision, 
3. leverages the state-of-the-art in software model checking and abstract interpretation for verification, and 
4. uses Horn-clauses as an intermediate language to represent verification conditions which simplifies interfacing with multiple verification tools based on Horn-clauses. 

SEAHORN provides users with a powerful verification tool and provides researchers with an extensible and customizable framework for experimenting with new software verification techniques.

ABSTRACT. In the frame of our previous experiments for proof based synthesis of sorting algorithms for lists and for binary trees, we employed certain special techniques which are able to generate multiple variants of sorting and merging, by investigating all combinations of auxiliary functions available for composing objects (lists, respectively trees). The purpose of this paper is to describe this technique and the results obtained. We present the main principles and the application of this technique to merging of sorted binary trees into a sorted one. Remarkably, merging requires a nested recursion, for which an appropriate induction principle is difficult to guess. Our method is able to find it automatically by using a general Noetherian induction and the combinatorial technique.

ABSTRACT. One of the core problems in real-time systems, finding a feasible schedule for a certain task set, is subject to alternative solutions given the various system constraints. While preemptive scheduling has benefited from a large number of significant results, the non-preemptive case has still room for improvement. This paper extends our previous results regarding the minimum number of processors required for getting a feasible schedule and the possible ways of improving the well known traditional scheduling algorithms in the case of non-preemptive, multiprocessor systems. The improvements refer to handling the situations when the already determined minimum number of processors proves insufficient, and also to extending an existing technique which allows the algorithm to overcome some stalling situations.

ABSTRACT. In this paper we sketch out a smart home system (and the reasoning mechanism behind it) designed to improve the living experience of the severly impaired, relying on logic, brain-computer interfacing (BCI) and mobile sensor agents. The exists a significant social category of people who due to either old age or conditions such as paralysis lose their ability to manage their own lives. Such persons are compelled to rely on others in order to manage their finances, expenses, daily necessities such as eating or turning on the television or dialing an emergency number. In our previous research we have described a manner in which to model emotions, as captured via BCI. Here, we extend this model to abstract and concrete concepts and employ epistemic logic and a logic of trust in order to allow communication between the person and heterogenous agents via a BCI headset. We firstly describe a formal model for expressing reasoning as captured in its cortical projection. Secondly, we describe a communication protocol that uses a logic of trust that allows the user to give commands to specific listening agents. The system should use reasoning and logic to learn from the user commands they receive and configure routines that correspond to the usual preferences and needs. Finally, the agents, on receiving and corroborating data from other sensors that relate to vital signs of the user or that otherwise identify a crisis situation, should be able to decide when to change their task priorities and the system should ad hoc self-configure in order to provide best assistance to the user.

ABSTRACT. Venn diagrams for sets are in use for more than a century. Multiset theory developed in the last decades, and although it has many applications in mathematics and computer science, remains relatively modest compared to set theory. We introduce Venn diagrams for finite multisets and show how they simplify the analysis of multisets and their submultisets. Venn diagrams are very useful in proofs involving multisets and multiset orders, especially considering the complications introduced by the multiplicity of elements in multisets.

We compare the Venn diagrams for finite multisets with the corresponding Venn diagrams for sets. Thus, we present two types of Venn diagrams for finite multisets, a simple one that looks like a diagram for sets, but with areas that are not necessarily disjoint, and a complex one (compared to sets), but with disjoint areas.

We show by examples that by using diagrams in a proof involving multisets the chance of making mistakes decreases significantly, in contradiction to the usual belief that diagrams tend to introduce errors in proofs.

ABSTRACT. Differential privacy has recently grabbed the attention of many privacy researchers. It provides a way to get useful information about sensitive data without revealing much about any one individual. It enjoys many nice compositionality properties not shared by other approaches to privacy, including, in particular, robustness against side-knowledge.
Designing differentially private mechanisms from scratch can be a challenging task. One way to make it easier to construct new differential private mechanisms is to design a system which allows more complex mechanisms (programs) to be built from differentially private building blocks in principled way, so that the resulting programs are guaranteed to be differentially private by construction. In this talk I will review the basic ideas of differential privacy and describe a new accounting principle for building differentially private programs. It is based on a simple generalisation of classic differential privacy which we call Personalised Differential Privacy, in which each individual has its own personal privacy budget. We will describe how this can be implemented in an interactive query system using the concept of lineage tracing from database theory.
(Describing joint work with Hamid Ebadi and Gerardo Schneider)

ABSTRACT. In this tutorial we focus on how to protect the confidentiality of user data in web applications in the presence of active attackers. In particular, driven by the architecture of a typical web application, we focus on the scenario where the attacker is able to inject malicious code into the application. By injecting code into the application the attacker is able to access and steal all data the application has access to, unless additional security mechanisms are put into place. The question to which we have been seeking the answer is how such mechanism might be constructed.

The tutorial is built around JSFlow [1], a security-enhanced JavaScript interpreter employing fine grained tracking of information-flow, and a simplified example web application, Hrafn, constructed to be open for various code injection  attacks, e.g., via buggy or compromised 3rd party services or via malicious user content.

Based on different practical attacks against Hrafn we illustrate the power of code injection attacks and discuss the current protection mechanism and their weaknesses. Thereafter we show how dynamic information-flow control provides a uniform line of defense against the attacks both in theory and in practice, using JSFlow. At the very end, we leave the focus on the client side to briefly discuss how information flow control can be leveraged on an application-wide level to provide confidentiality of user data.

ABSTRACT. As a general rule, each user must provide the used tool with particular values of its input parameters. An inexperienced user may hardly figure out their values and the tool developer must define their default values in order to help her/him. The used tool implements an algorithm, based on some model of reality. The model is as good as the data, measured in the reality and on the model are close. The problem under our investigation is to determine automatically the "good" default parameters. We provide the user with an advanced analytical method to help her/him to make better decisions about the values of the required parameters.

In this paper, we present an approach to solve the problem with the help of multi-criteria optimization that is new in this formulation. We demonstrate our approach in closer details using an example from the automatic definition of optimal default parameters for real-time merging of visual objects. However, our making decisions approach is generic and may be used for any kind of such inverse problems.

ABSTRACT. Forecasting has always been of interest. Whether one’s field is finance, health or seismology, being able to predict future values based on previously gathered data proves to be invaluable when taking decisions about that future. In this paper, we research machine learning techniques for prediction on time series and choose the best models that fit our use case, Smart Farm, in which we distributedly analyze time series received from farm-monitoring sensors. On time series with short term dependencies, like temperature or pressure, we make predictions with Hidden Markov Models, whilst for those with long range dependencies, like ground wind speeds or precipitations, we use Recurrent Neural Networks with Long Short-Term Memory architecture.

ABSTRACT. In this paper we present a real-time, continuous vital signs monitoring system based on a Multi-agent architecture. Real-time remote monitoring of the patient’s vital signs and generating alerts in case of emergency situations is of great importance in healthcare. Several tiny sensors attached on the patient’s body can collect physiological measurements of vital signs, and transmit them to a remote server, from where it can be consulted by a physician. Using Wireless Body Area Networks (WBANs) technology patients can move freely and perform daily tasks while being monitored. In such systems energy is the most valuable resource. Most energy is consumed by data transmission related operations. Therefore local processing of vital signs and continuously updating vital signs thresholds, according to the activity caried by the patient, on each sensor node, and sending data only when abnormal values exceed these ranges, can significantly reduce data transmission and save battery life.