Feedback control is pervasive in our lives, as it often lays the foundation of technology we daily interface with. Control systems are at the core of the energy distribution infrastructure, govern the behavior of vehicles, and are embedded into household appliances like washing machines. Controllers usually use sensors, that provide information about the physical environment, to calculate the values that actuators should assume to fulfill specific requirements. For example, adaptive cruise control systems use the throttle to automatically adjust the vehicle's speed, while maintaining a safe distance from vehicles ahead.

The actuator values are calculated using hardware and software. Hence, the computation of the new control signals is subject to accidental faults, systematic issues, and software bugs. However, in many cases, these computational problems can safely be ignored. This talk will introduce the problem of analyzing the behavior of control software subject to computational problems, and verifying when no corrective action is needed, i.e., when the control software is able to fulfill the system requirements despite the presence of computational problems.

Cyber-Physical Systems (CPS) are technical systems where a large software stack orchestrates the interaction of physical and digital components. Such systems are omnipresent in our daily life and their correct behavior is crucial. However, developing safe, reliable and performant CPS is challenging. A promising research direction towards this goal is the combination of formal methods from computer science and controller synthesis techniques from automation.

In my talk I will discuss how infinite two-player games over finite graphs, originating from the formal methods community, can be utilized and enhanced for higher layer control of CPS. In particular, I will discuss how the use of environment assumptions - used to model particularities of the system under control within these games - has to be rethought in order to effectively solve controller synthesis tasks for CPS.

Sortition is a storied paradigm of democracy built on the idea of choosing representatives through lotteries instead of elections. In recent years this idea has found renewed popularity in the form of citizens’ assemblies, which bring together randomly selected people from all walks of life to discuss key questions and deliver policy recommendations. A principled approach to sortition, however, must resolve the tension between two competing requirements: that the demographic composition of citizens’ assemblies reflect the general population and that every person be given a fair chance (literally) to participate. I will describe our work on designing, analyzing and implementing randomized participant selection algorithms that balance these two requirements. I will also discuss practical challenges in sortition based on experience with the adoption and deployment of our open-source system, Panelot.

Recent years have seen tremendous progress in the development and industrial adoption of rigorous techniques and tools to automatically detect bugs in software and ensure its correctness. Static program analysis is one such technique to automatically reason about the runtime behavior of a program without actually running it. It is a powerful approach that can be used to detect a wide range of security vulnerabilities and enables program optimization in compilers, automatic parallelization, and, if accurate enough, correctness verification. Static program analyzers are tools that implement program analysis techniques and are used to analyze other programs for flaws. Decades of research have yielded the discovery of novel algorithms, data structures, and design principles that make static program analysis tools and techniques more precise, scalable, and faster than ever before.

While the potential benefits of analyzers are obvious, their usability and effectiveness in mainstream software development workflows still often comes into question. This is because the undecidability of the halting problem makes formal reasoning about program properties difficult. Therefore, one common theme in static analysis is that to remain computable, one has to sacrifice either soundness or completeness. This means that, in practice, a static analysis technique might either miss a bug (false negative) or report correct code as having a bug (false positive), might not handle certain language features, or might only report certain types of bugs.

Practical program analyzers have to make tradeoffs (e.g., in soundness, precision, or performance) to maintain a delicate balance between returning the minimum number of false negatives/positives, scaling to very large industrial codebases, being highly automatic, and having minimum overhead for the developers. Designing, implementing, and deploying program analyzers, therefore, is an extremely challenging task. This makes them extremely complicated pieces of software with a high likelihood of having correctness bugs themselves (challenge 1) or tradeoffs not suitable for every piece of code under every usage scenario (challenge 2).

In this dissertation, we focus our attention on improving the state of the art in the above two challenge areas that can prevent typical software development teams from using these tools to their full potential. In the first part of the dissertation, we present algorithms to detect correctness bugs in fundamental program analysis components such as SMT solvers and Datalog engines. Correctness issues in program analyzers can have disastrous consequences e.g. when analyzing software used for electronic voting, financial systems, transportation, or secure communication. In the second part, we introduce techniques to reduce friction in the integration of program analyzers in everyday software development workflows. Smoothly integrating and tuning an advanced program analyzer for a particular codebase under certain resource constraints and different usage scenarios can be a challenging task for software developers, most of whom lack an advanced understanding of these analyzers.

Given an integer n ≥ 2, let P (n) stand for its largest prime factor. Given integers k ≥ 2 and ℓ ≥ 2, consider the set Ek,ℓ of those integers n ≥ 2 for which P (n + i)ℓ | n + i for i = 0, 1, . . . , k. Each of these sets is very small. For instance, the smallest element of E3,2 is 1 294 298, the smallest known element of E3,3 has 77 digits and no elements of E4,2 are known, even though all these sets are believed to be infinite. In this talk, using elementary, analytic and probabilistic approaches, we will shed some light on these sets and raise several open problems. This is joint work with Nicolas Doyon, Florian Luca and Matthieu Moineau.

---

This talk will be a hybrid event. You can join the meeting in E1 5 room 002 in Saarbrücken, in G26 room 111 in Kaiserlautern or via Zoom. Please contact the Office team for Zoom link information.