Events

tbd

tbd

Sound static analysis over-approximates the set of all possible executions in a given program in order to prove the absence of errors in the program. Due to this over-approximation, sound static analysis may generate spurious warnings about executions that are not wrong or even possible in the program. To become more practical, many static analyzers give up soundness by design. This means that they do not check certain properties or that they check them under certain unsound assumptions, such as the absence of arithmetic overflow. At the other end of the soundness spectrum, we have automatic test-case generation, which typically under-approximates the set of possible program executions. The goal of test-case generation is not to prove the absence of errors in the program but, rather, their existence. In this talk, I will present an overview of my research on combining these program analysis techniques to improve their overall automation, performance, and accuracy on real programs.

Twenty years ago we were able to repair cars at home. Nowadays customer services repair coffee machines by installing software updates. Soon you will no longer be able to repair your bike.

Embedded software innovations boost our society; they help us tremendously in our daily life. But we do not understand what the software embedded therein actually does, regardless of how well educated or smart we are. Proprietary embedded software has become an opaque layer between functionality and user. That layer is thick enough to possibly induce malicious or unintended behaviour, as it happened massively in our diesel cars. From the outside, there is no understanding of how decisions are made inside and across these software-driven black boxes. The outcomes are often not designed to be accessible, verified or evaluated by humans, limiting our ability to identify if, when, where, and why the software produced harm -- and worse still -- redress this harm. Proprietary embedded software locks us out of the products we own.

The presentation of Holger Hermanns will sketch the main cornerstones of a research agenda which targets the foundations of open and hence customisable embedded software. A minor customisation might well have strong unexpected impact, for instance on the longevity of an embedded battery, or the safety of the battery charging process. Means to detect, quantify and prevent such implications are needed. Those are delivered by quantitative verification technology for system-level correctness, safety, dependability and performability. Hermanns will link foundational achievements to concrete results in the area of power management for electric mobility and for satellite operation. Electric power is intricate to handle by software, is safety-critical, but vital for mobile devices and their longevity. Since ever more tools, gadgets, and vehicles run on batteries and use power harvesting, electric power management is itself a pivot of the future.

I will speak about an unexpected correspondence between a beautiful theory, due to Lovasz, about homomorphisms and graph limits and a popular heuristic for the graph isomorphism problem known as the Weisfeiler-Leman algorithm. I will also relate this to graph kernels in machine learning. Indeed, the context of this work is to desgin and understand similarity measures between graphs and discrete structures.

Distributed real-time (DiRT) systems are widely deployed in contemporary cyber-physical systems (CPS). Many of these systems are safety-critical, since their failure or malfunction can result in death or serious injuries to the people and/or severe damage to the environment involved, e.g., human spaceflight vehicles, surgical robots, air traffic and nuclear reactor control systems, drive-by-wire and fly-by-wire systems, railway signaling systems, etc.

Safety-certification standards mandate that the failure rate of safety-critical systems in the presence of any unpreventable and intolerable errors due to environmentally-induced transient faults (such as due to electromagnetic, thermal, and radiation sources) must be under a certain threshold.

In this regard, prior work on the reliability analysis of DiRTs in the presence of environmentally-induced transient faults does not target all possible error scenarios (such as Byzantine errors). This is mainly because the likelihood of a complex error scenario is extremely low and/or because the workloads for safety-critical systems have traditionally been simple, with sufficient slack to tolerate fault-induced failures and with mechanical backups to tolerate complete software failures.

However, a majority of CPS devices are expected to be fully autonomous in future, thus requiring stronger reliability guarantees with fail-operational semantics. In addition, since the workloads used for safety-critical systems are becoming more and more complex (e.g., deep learning neural networks are being used in self-driving cars) and since there is a push towards the use of cheaper community hardware, the likelihood of complex Byzantine errors is going to increase. Therefore, it is imperative that we revisit the existing techniques for analyzing and building safety-critical DiRTs.

To address this issue, we propose analyses to derive a safe upper-bound on the failure rates of safety-critical DiRTs in the presence of Byzantine errors due to environmentally-induced transient faults. We focus on DiRTs based on Controller Area Network that are commonly used in today's cyber-physical systems, and on Ethernet-based DiRTs that are expected to be at the core of next-generation cyber-physical systems.