Viinistu, Estonia, March 3 - 6, 2025
Anders Claesson
(Professor at University of Iceland, Iceland)
Combinatorial species
The answer to an enumerative combinatorics problem is typically a sequence of natural numbers. However, combinatorialists rarely work directly with this sequence; instead, they find it more convenient to work with a power series whose coefficients form the sequence of interest, known as a generating series. Combinatorial species can be viewed as a "categorification" of generating series. Formally, a species is defined as an endofunctor on the category (or groupoid) of finite sets and bijections. Moreover, operations such as addition, multiplication, composition, and differentiation are defined on species in a way that mimics those on generating series. This allows us to express relationships between combinatorial objects using algebraic expressions and equations (isomorphisms). Another benefit of species is that they inherently carry the necessary information for defining their unlabeled counterparts.
We aim to provide a concrete and accessible introduction to the theory of combinatorial species. No prior knowledge of category theory is assumed or required. We will explore familiar combinatorial families (data structures), such as sets, linear orders (lists), permutations, graphs, and trees, using the framework of combinatorial species. Highlights include a species-based solution to Montmort's (1713) classic hat-check problem and Joyal's (1981) brilliant proof of Cayley's (1889) formula for counting trees.
Uli Fahrenberg
(Professor at LRE, EPITA Rennes, France)
Discrete and continuous models for concurrent systems: from Petri nets to directed spaces
Concurrent computing systems are those in which several events may happen in parallel; in fact that includes most modern systems. The verification of such systems is difficult: if one considers all possible interleavings of concurrent events, thus reducing concurrent systems to sequential systems which are well-understood, then the state space explodes; in addition it is not clear a priori which interleavings are possible (think out-of-order executions).
Perhaps surprisingly, geometry and topology may provide plenty of intuition for analysing concurrent systems in their own right, i.e. without reducing them to sequential systems. We will use this as a guiding principle for introducing several models for concurrent systems, exploring the relations between them, and using them for verification.
The course will cover Petri nets, concurrent step transition systems, higher-dimensional automata, and directed topological spaces. We will see how to translate these formalisms into each other, how to analyse them, and how to use them to model concurrent systems. If time permits, we will also look at extensions such as Petri nets with inhibitor arcs or higher-dimensional timed automata.
Miika Hannula
(Associate Professor at University of Tartu, Estonia)
Conjunctive query evaluation
Query evaluation is one of the most central problem in databases. Given a query q, a value c, and a database D, this problem is to determine whether c belongs to the output q(D) of the query q on the database D. Remarkably, this problem is NP-complete even for conjunctive queries, which correspond to the most basic kind of SQL queries. What explains, then, that databases are so successful in practice? This course explores the theoretical foundations and techniques that make efficient query evaluation possible.
The first half of the course examines how concepts and tools from logic, graph theory, and information theory are applied to analyze and optimize conjunctive query evaluation. The second half addresses conjunctive query evaluation in the presence of uncertainty, focusing on consistent query answering—a framework designed for querying databases with inconsistent information. By the end of the course, students will understand how theoretical principles underpin the possibilities and limitations of query evaluation in database systems.
Marino Miculan
(Associate Professor at University of
Udine, Italy)
Formally Verifying Security of Complex Architectures: MFA and Containerized Systems
The inherent complexity of modern information systems, arising from composition of concurrent, distributed, and heterogeneous components, poses significant challenges to security and analysis. In this course we examine the role of formal methods in developing models and tools suitable for rigorous verification, with a focus on the concepts of composition and interface.
The course is divided into two parts. First, we introduce ProVerif, a leading automatic cryptographic protocol verifier within the formal Dolev-Yao model. We then present a methodology for formally modeling and verifying multi-factor authentication (MFA) schemes, using eIDAS digital identity cards as a practical example. This methodology employs an interface-based threat model to comprehensively analyze potential vulnerabilities and enumerate threat scenarios based on attacker's capabilities. Using Italy's CIE (Carta d'Identit? Elettronica) as a case study, we demonstrate how to automatically generate ProVerif models of these scenarios, revealing vulnerabilities. We propose and formally verify minor protocol modifications to address these vulnerabilities.
The second part of the course focuses on containerized systems, the foundation of modern service-oriented architectures. We present a formal model for these systems based on Bigraphical Reactive Systems (BRSs). This formal representation facilitates the analysis and manipulation of containerized systems using graph-theoretic techniques. Finally, we introduce DBCChecker, a prototype tool that, given descriptions of container interfaces, behaviors, and compositions, constructs a formal model analyzable by ProVerif, enabling the verification of critical security properties like integrity and confidentiality.
10:30 - 11:00 | Arrival and setting up |
11:00 - 11:30 | Welcome coffee |
11:30 | Opening |
11:45 - 12:45 | Uli Fahrenberg "Discrete and continuous models for concurrent systems: from Petri nets to directed spaces" I |
13:00 | Lunch and break |
14:30 - 15:30 | Anders Claesson "Combinatorial species" I |
15:30 - 16:00 | Coffee break |
16:00 - 17:00 | Marino Miculan "Formally Verifying Security of Complex Architectures: MFA and Containerized Systems" I |
17.00 - 17.15 | Break |
17.15 - 18.15 | Exercises in Purekkari and Mohni Halls |
19:00 | Dinner and discussions |
08:00 - 08:45 | Breakfast |
09:00 - 10:00 | Miika Hannula "Conjunctive query evaluation" I |
10:00 - 10:30 | Coffee break |
10:30 - 11:30 | Uli Fahrenberg "Discrete and continuous models for concurrent systems: from Petri nets to directed spaces" II |
11:30 - 11:45 | Break |
11:45 - 12:45 | Anders Claesson "Combinatorial species" II |
13:00 | Lunch |
14:30 - 15:30 | Marino Miculan "Formally Verifying Security of Complex Architectures: MFA and Containerized Systems" II |
15:30 - 16:00 | Coffee break |
16:00 - 17:00 | Miika Hannula "Conjunctive query evaluation" 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 |
08:00 - 08:45 | Breakfast |
09:00 - 10:00 | Uli Fahrenberg "Discrete and continuous models for concurrent systems: from Petri nets to directed spaces" III |
10:00 - 10:30 | Coffee break |
10:30 - 11:30 | Anders Claesson "Combinatorial species" III |
11:40 - 13:10 | Visiting Viinistu Art Museum. |
13:10 | Lunch |
14:30 - 15:30 | Miika Hannula "Conjunctive query evaluation" III |
15:30 - 16:00 | Coffee break |
16:00 - 17:00 | Marino Miculan "Formally Verifying Security of Complex Architectures: MFA and Containerized Systems" III |
17:00 - 17:15 | Break |
17.15 - 18.15 | Exercises in Purekkari and Mohni Halls |
19:00 | Dinner and discussions |
20:30 ... | CRAPcon 2025 ??? in Purekkari Hall |
08:00 - 08:45 | Breakfast |
09:00 - 10:00 | Anders Claesson "Combinatorial species" IV |
10:00 - 10:30 | Coffee break and check-out |
10:30 - 11:30 | Miika Hannula "Conjunctive query evaluation" IV |
11:30 - 11:45 | Break |
11:45 - 12:45 | Marino Miculan "Formally Verifying Security of Complex Architectures: MFA and Containerized Systems" IV |
13:00 | Lunch |
14:30 - 15:30 | Uli Fahrenberg "Discrete and continuous models for concurrent systems: from Petri nets to directed spaces" 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'25 is the twenty seventh event of the series.
To apply for a place, fill in the online participation application form before February 12, 2025.
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: 490 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 sponsored by the Department of Software Science of Tallinn University of Technology.
WEBPAGEhttps://cs.ioc.ee/ewscs/2025/ |
EMAIL CONTACTewscs25 (at) cs.ioc.ee |
Last changed
February 3, 2025 12:25 EET (GMT +02:00)
by local organisers