Courses at EWSCS 2025

• Anders Claesson (professor at University of Iceland, Iceland)
  Combinatorial species   toggle abstract   (course details)

  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   toggle abstract   (course details)

  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   toggle abstract   (course details)

  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 (professor at University of Udine, Italy)
  Formally verifying security of complex architectures: multi-factor authentication and containerized systems   toggle abstract   (course details)

  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.

  ---

PROGRAMME

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.

• Peeter Laud (Cybernetica AS)
• Monika Perkmann (Tallinn University of Technology)
• Pille Pullonen-Raudvere (Cybernetica AS)
• Ago-Erik Riet (University of Tartu)
• Tarmo Uustalu (Reykjavik University / Tallinn University of Technology)

The school is organised by Cybernetica AS. The school is sponsored by the Department of Software Science of Tallinn University of Technology.