Viinistu, Estonia, March 4 - 7, 2024
Szabolcs Horvát
(Assistant Professor at Reykjavik University, Iceland)
Random graphs and methods for constructing them
In this lecture series we will look at the problem of generating random
graphs with various prescribed properties, and investigating them. How
do we generate a random tree, chosen uniformly from the set of all
trees on n vertices? What is an efficient algorithm for creating a
random graph with a given number of edges? What is the probability that
it will be connected? What about generating random connected graphs
with prescribed degrees? What if we only specify the average degree of
each vertex (a so-called "soft" constraint)?
So-called random graph models—statistical distributions over the set of
graphs—find many practical applications. They are one of the
fundamental tools for studying real-world network data, and are
commonly used as statistical null models. In order to make effective
use of them we need unbiased and efficient sampling algorithms for
graph. In these lectures we will learn about different kinds of random
graph models (including maximum entropy models), and will look at
techniques for constructing sampling algorithms for them.
Meiko Jensen
(Senior Lecturer at Karlstad University, Sweden)
From anonymization to protection goals for privacy engineering
Effective protection of sensitive personal data is one of the biggest
challenges in IT systems these days. Technical means to enhance security
and privacy of such data therefore are key topics in today's computer
science education globally.
In this lecture, I will focus on a selected set of privacy-enhancing
technologies (PETs) that can be implemented to safeguard data processing
in a secure and legally compliant manner. I will iterate over the six
classical protection goals of privacy and security, briefly discuss
relevant legal and economic requirements, and provide some core insights
into anonymization and pseudonymization techniques, as well as other
relevant privacy concepts in use today.
Elaine Pimentel
(Associate Professor at University College London, UK)
Proof theory for ecumenical systems
Ecumenism can be understood as a pursuit of unity, where diverse thoughts, ideas, or points of view coexist harmoniously. In logic, ecumenical systems refer, in a broad sense, to proof systems for combining logics. One captivating area of research over the past few decades has been the exploration of seamlessly merging classical and intuitionistic connectives, allowing them to coexist peacefully.
In this tutorial, we will embark on a journey through ecumenical systems, drawing inspiration from Prawitz’ seminal work [8]. We will begin by elucidating Prawitz’ concept of “ecumenism” and present a pure sequent calculus version of his system. Building upon this foundation, we will expand our discussion to incorporate alethic modalities, leveraging Simpson’s meta-logical characterization. This will enable us to propose several proof systems for ecumenical modal logics.
We will conclude our tour with some discussion towards a term calculus proposal for the implicational propositional fragment of the ecumenical logic, the quest of automation using a framework based in rewriting logic, and an ecumenical view of proof-theoretic semantics.
César Sánchez
(Full Research Professor at the IMDEA Software Institute, Spain)
Temporal logics for hyperproperties
Formal verification is the problem of a system satisfies a
specification. A common language to express behaviors is Linear
Temporal Logic (LTL) a modal logic to express temporal properties of
single traces of the execution of a system. A system satisfies an LTL
specification if all executions conform to it.
Hyperproperties are properties of systems that require to reason
simultaneously about multiple traces of the system under
analysis. Examples include security policies such as noninterference,
non-inference, observational determinism, declassification, etc and
other properties like symmetry of schedulers and correctness of
coding/decoding systems. Unfortunately, standard temporal logics,
like only refer to a single path at a time and cannot express many
hyperproperties of interest.
In these talks, I will revisit LTL with many examples and describe its
model checking problem. Then, I will introduce HyperLTL, which extends
LTL and with quantification over multiple paths. I will also show
many examples of properties in this logic, and then introduce model
checking algorithms, including a bounded model checking approach.
I will then present extension of HyperLTL for real-time and
asynchronous properties where the different traces of execution can
evolve at different speeds. Finally, I will present open problems and
current avenues for research.
10:30 - 11:00 | Arrival and setting up |
11:00 - 11:30 | Welcome coffee |
11:30 | Opening |
11:45 - 12:45 | Szabolcs Horvát "Random graphs and methods for constructing them" I |
13:00 | Lunch and break |
14:30 - 15:30 | Elaine Pimentel "Proof theory for ecumenical systems" I |
15:30 - 16:00 | Coffee break |
16:00 - 17:00 | Meiko Jensen "From anonymization to protection goals for privacy engineering" I |
17.00 - 17.15 | Break |
17.15 - 18.15 | Exercises in Purekkari and Mohni Halls |
19:00 | Dinner and discussions |
21:00-24:00 | Sauna I |
08:00 - 08:45 | Breakfast |
09:00 - 10:00 | César Sánchez "Temporal logics for hyperproperties" I |
10:00 - 10:30 | Coffee break |
10:30 - 11:30 | Szabolcs Horvát "Random graphs and methods for constructing them" II |
11:30 - 11:45 | Break |
11:45 - 12:45 | Elaine Pimentel "Proof theory for ecumenical systems" II |
13:00 | Lunch |
14:30 - 15:30 | Meiko Jensen "From anonymization to protection goals for privacy engineering" II |
15:30 - 16:00 | Coffee break |
16:00 - 17:00 | César Sánchez "Temporal logics for hyperproperties" II |
17:00 - 17:15 | Break |
17.15 - 18.15 | Exercises in Purekkari and Mohni Halls |
19:00 | Dinner and discussions |
21:00-24:00 | Sauna II |
08:00 - 08:45 | Breakfast |
09:00 - 10:00 | Szabolcs Horvát "Random graphs and methods for constructing them" III |
10:00 - 10:30 | Coffee break |
10:30 - 11:30 | Elaine Pimentel "Proof theory for ecumenical systems" III |
11:40 - 13:10 | Visiting Viinistu Art Museum. |
13:10 | Lunch |
14:30 - 15:30 | César Sánchez "Temporal logics for hyperproperties" III |
15:30 - 16:00 | Coffee break |
16:00 - 17:00 | Meiko Jensen "From anonymization to protection goals for privacy engineering" III |
17:00 - 17:15 | Break |
17.15 - 18.15 | Exercises in Purekkari and Mohni Halls |
19:00 | Dinner and discussions |
20:30 ... | CRAPcon 2024 in Purekkari Hall |
08:00 - 08:45 | Breakfast |
09:00 - 10:00 | Elaine Pimentel "Proof theory for ecumenical systems" IV |
10:00 - 10:30 | Coffee break and check-out |
10:30 - 11:30 | César Sánchez "Temporal logics for hyperproperties" IV |
11:30 - 11:45 | Break |
11:45 - 12:45 | Meiko Jensen "From anonymization to protection goals for privacy engineering" IV |
13:00 | Lunch |
14:30 - 15:30 | Szabolcs Horvát "Random graphs and methods for constructing them" IV |
15:30 - 15:40 | Closing |
15:45 | Departure (bus) |
EWSCS is a series of regional-scope international winter schools held annually in Estonia.
The main objective of EWSCS is to expose Estonian, Baltic, and Nordic graduate students in computer science (but also interested students from elsewhere) to frontline research topics usually not covered within the regular curricula. The working language of the schools is English.
EWSCS'24 is the twenty sixth event of the series.
To apply for a place, fill in the online participation application form before February 19, 2024.
Admitted participants will be expected to attend all of the school's program. They will be provided access to materials of the courses. Participation includes 3 nights accommodation in twin rooms with full board.
Participation fee: 450 EUR; we may be able to reduce the fee for some BSc and MSc students.
The school will take place at Viinistu Art Hotel. Viinistu is a fishing village in Kuusalu Parish, Harju County in northern Estonia within the territory of Lahemaa National Park. It is located on the coast of the Gulf of Finland on the Pärispea Peninsula by the Eru Bay, about 7 km north of the town of Loksa. From Tallinn the distance is 77 kms.
The school will organize a bus from Tallinn to Viinistu and back.
The school is organised by Cybernetica AS. It is sponsored by the Department of Software Science of Tallinn University of Technology.
WEBPAGEhttps://cs.ioc.ee/ewscs/2024/ |
EMAIL CONTACTewscs24 (at) cs.ioc.ee |
Last changed
April 9, 2024 11:08 EEST (GMT +03:00)
by local organisers