Simon Rehwald from itestra will give a talk in the elite program’s special lecture series. The title of the talk is “Agile Entwicklung – Herausforderungen und Irrwege” and it will take place in room 1055N at 4PM on 17 July 2025.

Abstract

Agile Methoden wie SCRUM sind inzwischen Standard in der Softwareentwicklung bei vielen Unternehmen. Mit der breiten Anwendung kommt es allerdings auch zu Missinterpretationen: Anstelle der ursprünglichen Fokussierung auf die Produktion nutzbringender lauffähiger Software durch flexible Teams dominieren dann starre Prozesse, Overhead durch kleinteilige Sprintplanung und Ziellosigkeit. Ein erfahrener Entwickler, Projektleiter und Berater der itestra GmbH zeigt mit Praxisbeispielen aus verschiedenen Unternehmen, welche agilen Elemente wann Sinn machen, welche Alternativen es gibt und worauf man achten sollte.

Florian Lercher from TUM will give a talk in the elite program’s special lecture series. The title of the talk is “No More Traffic Tickets: Ensuring Traffic-Rule Compliance of Automated Vehicles” and it will take place in room 1055N at 4PM on 10th July 2025.

Abstract

Imagine an automated vehicle violating a traffic rule and, by that, causing an accident. This would not only be devastating for a responsible operator, but, more importantly, each such incident erodes the trust of the public in automated vehicles. Fortunately, compliance with traffic rules can be fully controlled unless other traffic participants breach them — this causality makes it possible for responsible operators to avoid liability claims. Despite their importance, traffic rules are often only implicitly embedded in various fragments of the software stack of automated vehicles. However, traffic rule compliance should be ensured by formal methods to gain the necessary trust of the public. To this end, traffic rules should be represented explicitly and provided centrally.

Using a running example, this talk provides an overview of the steps required to achieve this goal. We start by formalizing traffic law to obtain an explicit representation in temporal logic. Based on this, we design a motion planning pipeline comprising three steps: reachability analysis to narrow the search space for rule-compliant trajectories, trajectory planning within the narrowed search space, and trajectory repairing to ensure rule-compliance of planned trajectories. Moreover, we always keep a fail-safe trajectory ready to safely react to unexpected behavior of other traffic participants.

Biograpyh

Florian Lercher is a graduate of the elite program Software Engineering and works on his Ph.D. at the Cyber Physical Systems Group at TUM.

Dr. Johannes Leupolz will give a talk in the elite program’s special lecture series. The title of the talk is “Qualitative and quantitative analysis of safety-critical systems with S#” and it will take place in room 1055N at 10AM on 10th July 2025.

Abstract

Safety-critical systems are expected to operate safely under regular circumstances as well as in many degraded situations. In the latter case, these systems have to cope with one or more components that are not working as specified, while at the same time they have to avoid (serious) economical or environmental damage, injuries, or even loss of lives. S# provides a modeling language specifically designed to express important safety-related concepts such as faults and the physical environment of a safety-critical system. For safety assessments, model simulations as well as formal safety analyses are supported.

Emily Schiller and Anton Hummel from XITASO will give a talk in the elite program’s special lecture series. The title of the talk is “Explainable AI and Uncertainty Quantification” and it will take place in room 1055N at 4PM on 26th June 2025.

Abstract

Despite the transformative potential of machine learning in critical areas such as healthcare, its integration is challenged by a lack of trust and acceptance. To overcome these challenges by ensuring reliant decision-making the interaction of users and the AI systems is crucial. Two research fields have the potential to improve human-AI collaboration: Explainable AI and Uncertainty Quantification. Explainable AI (XAI) aims to make AI predictions interpretable for humans. At the same time, Uncertainty Quantification (UQ) enables the estimation of confidence in predictions. Both areas have made important contributions to trustworthy AI, but to fully realize their potential they must be tailored to the needs of the end-users. In this presentation, we show what is needed to create a practical value in AI by highlighting novel XAI and UQ methods.

Prof. Viktor Leis from TUM will give a talk in the elite program’s special lecture series. The title of the talk is “Towards Sanity in Query Languages” and it will take place in room 1055N at 4PM on 08th May 2025.

Abstract

The relational model has stood the test of time and is the foundation of most database systems. But let’s be honest — its success is not because of SQL, but in spite of it. SQL’s syntax is arcane, inconsistent, and bears little resemblance to the actual execution semantics of queries. Worse yet, SQL is not even a true standard — every system implements its own incompatible dialect, creating a fractured ecosystem where portability and interoperability are afterthoughts. This lack of standardization slows down innovation, forcing database developers to reinvent the wheel instead of pushing the field forward.

In this talk, we argue that we need a formally defined Sane Intermediate Representation (SaneIR) — a well-specified, interoperable abstraction for relational query execution. SaneIR would serve as a lingua franca between database systems, enabling compatibility, portability, and accelerated progress in the database world. It’s time to stop treating SQL as the immovable foundation of relational databases and start designing a future where database systems can truly evolve.

Philip Schäfer from QPLIX will give a talk in the elite program’s special lecture series. The title of the talk is “Putting Wealth Into Perspective – Understanding global wealth dynamics and opportunities in wealth management” and it will take place in room 1055N at 4PM on 15th May 2025.

Abstract

What is wealth, and how is it shaping the world? This talk takes you on a journey through the global wealth game — who owns what, how fortunes grow, and what’s changing. We’ll explore how the wealthy invest their money and uncover the different types of players managing money. What challenges do they face? What trends are reshaping the industry? Finally, we’ll look at how technology is transforming wealth management, with real-world examples from QPLIX. If you’re curious about finance, business, and the future of money, this talk will give you a fresh perspective on the world of  wealth.

Biography

Philip Schäfer is Director Client Solutions at QPLIX a graduate of the elite program Software Engineering.

The application period for the winter intake 2025 has started. For instructions on how to apply, please visit our application web-site.

Marian Lingsch-Rosenfeld from LMU will give a talk in the elite program’s special lecture series. The title of the talk is “Software Verification Witnesses” and it will take place in room 1055N at 4PM on 21st January 2025.

Abstract

Ensuring that software meets desired quality standards is a crucial aspect of the development process. A wide variety of approaches and tools exist for this purpose, with four important paradigms: Testing, Automatic Verification, Deductive Verification, and Interactive Theorem Provers. Each paradigm has unique strengths and limitations with notable tools including, but not limited to, AFL++ for Testing, Dafny and Frama-C for Deductive Verification, CPAchecker and UAutomizer for Automatic Verification, and KIV and Coq for Interactive Theorem Proving, between many others. Different tools differ not only in their underlying formalisms, which influence how they present proofs or counterexamples, but also in their preferred methods of interacting with users.

In this talk I will present an idea which has emerged in the last decade to aid in tool interoperability and user interaction: Software Verification Witnesses. Witnesses are a machine-readable data format that allows tools to encode information about their verification process as invariants for correctness arguments or paths through a program leading to an error.

Biography

Marian Lingsch-Rosenfeld is a graduate of the elite program Software Engineering and does his Ph.D. at LMU’s SoSy-Lab.

Dr. Andreas Angerer und Michael Brunner from XITASO will give a talk in the elite program’s special lecture series. The title of the talk is “Agile Entwicklung und langlebige Architekturen – wie passt das zusammen?” and it will take place in room 1055N at 4PM on 5th December 2024.

Abstract

In der agilen Softwareentwicklung ist iterativ-inkrementelles Vorgehen sowie kontinuierliches Refactoring auf allen Ebenen elementarer Bestandteil. Softwarearchitektur wird als Mittel zum Zweck – der Wertschöpfung – gesehen und ist kontinuierlich im Fluss. Was aber nun, wenn agile Softwareentwicklung auf sehr langlebige Produktionsmaschinen und deren eigene Architekturen trifft? Wie man in diesem Spannungsfeld navigieren, technische Schulden abbauen und regelmäßig Mehrwert durch Software liefern kann, stellen wir anhand von Erfahrungen aus langjährigen Entwicklungszusammenarbeiten mit Kunden aus dem Maschinen- und Anlagenbau vor.

Henrik Wachowitz from LMU will give a talk in the elite program’s special lecture series. The title of the talk is “Usability and Infrastructure: Challenges in Software Verification” and it will take place in room 1055N at 4PM on 28th November 2024.

Abstract

In this talk, I explore the field of automatic software verification and address a central question: why hasn’t formal verification gained wider adoption? My research emphasizes usability, seeking to make software verification more intuitive and accessible for developers.

I will introduce FM-Weck, a tool designed to streamline the exploration and integration of community tools by leveraging terminology familiar to software verification researchers. Additionally, I will present the CoVeriTeam GUI, a no-code framework that empowers users to build cooperative verification workflows effortlessly.

As part of the infrastructure challenges, I will present CPA-Daemon, a framework that makes the software verifier CPAchecker accessible via gRPC. This framework enables stateful verification, opening new possibilities for distributed and persistent analysis.

Finally, I will illustrate these themes through two key use cases: large-scale distributed software verification and the international Software Verification Competition (SV-COMP). These examples highlight the ongoing challenges and opportunities in advancing both the usability and infrastructure of software verification tools.

Biography

Henrik Wachowitz is a graduate of the elite program Software Engineering and does his Ph.D. at LMU’s SoSy-Lab.