State-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts for software using its symbolic encoding. In this talk, I will present a new application of CHCs to test-case generation, a problem of finding a set of tuples of input values to a program under which the program visits as many branches as possible. The key insight to achieve maximality is to identify and skip blocks of code that are provably unreachable. The new approach to test case generation called HORNTINUUM uses CHC to incrementally construct different program unrollings and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code which makes the unrolling process more efficient. In practice, this lets HORNTINUUM terminate early while guaranteeing maximal coverage. HORNTINUUM exhibits promising performance: it generates high coverage in the majority of cases and spends less time on average than state-of-the-art based on bounded model checking, concolic execution, and/or fuzzing.

The FIDE Laws of Chess establish that if a player runs out of time during a game, they lose unless there exists no sequence of legal moves that ends in a checkmate by their opponent, in which case the game is drawn. The problem of determining whether or not a given chess position is unwinnable for a certain player has been considered intractable by the community and, consequently, chess servers do not apply the above rule rigorously, thus unfairly classifying many games. We propose, to the best of our knowledge, the first algorithm for chess unwinnability that is sound, complete and efficient for practical use. We also develop a prototype implementation and evaluate it over the entire Lichess Database (containing more than 6 billion games), successfully identifying all unfairly classified games in the database.

Petri nets (PN) are a popular formalism to represent concurrent systems. However, they lack support for modelling and analysing system families, like variants of controllers, process models, or configurations of flexible assembly lines. a Petri net product line (PNPL) defines a collection of similar systems compactly. A PNPL represents a set of Petri nets with different admissible derivations. Having just one artefact allows for analysing all derivable nets of a family more efficiently at the same time, instead of one by one. Thus, PNPLs permit the analysis of structural and behavioural properties and the runtime verification of reconfigurable systems. In addition, a software tool has been developed to evaluate the benefits of our proposal.

Indirect surveys have been used for decades by epidemiologists and social scientists to estimate the size of sub-populations within social networks. In these surveys, respondents provide information about their social connections, making them particularly useful for monitoring hard-to-reach or sensitive populations, such as disaster casualties, drug use prevalence, or the spread of infectious diseases. These indirect responses, known as Aggregated Relational Data (ARD), are analyzed using various statistical methods collectively referred to as the Network Scale-Up Method (NSUM). However, to the best of our knowledge, no analytical bounds have been established for the estimation errors that may occur with NSUM.

In this seminar, we first focus on two popular NSUM estimators, demonstrating that in the worst-case scenario, the estimation error can be a factor of Ω(√n) away from the actual sub-population size, where n is the number of nodes in the network. Additionally, we prove that for random social networks, a small constant error factor can be achieved with high probability using logarithmic-sized samples.

We then focus to the application of indirect online surveys for continuous data collection. While NSUM can be applied by analyzing data independently at each time point, this approach overlooks the potential benefits of leveraging temporal data. Instead, we propose an approach that uses ARD collected over time, proving that indirect surveys can provide more accurate estimates of sub-population trends compared to direct surveys. Additionally, we identify appropriate methods for temporal aggregation to further enhance the accuracy of these estimates.

This talk starts with a result in classical Finite Automata Theory: Two regular languages with the same number of words for each length can be mapped one onto the other by a letter-to-letter (finite) transducer. The notion of generating function of regular languages leads to the in- troduction of the model of weighted automata. The conjugacy of weighted automata, a concept borrowed to symbolic dynamics, is then defined and it is shown how the above statement can be derived from the central result of this work: Two equivalent weighted automata are conjugate to a third one when the weight semiring is B, N, Z, or any Euclidean domain (and thus any (skew) field). This talk is based on a joint work with Marie-Pierre Béal and Sylvain Lom- bardy.