Time and Place

  • Time: May 30, 2023, 9:00 – 15:00
  • Place: Lecture room T01, Jakob-Haringer-Straße 2, 5020 Salzburg
  • Registration: Please  register for the event to facilitate the planning.
  • Online Participation: All talks will be streamed in a  Teams meeting.


  • 09:00 Welcome
  • 09:05 Nikolaus Augsten: Research with Industry Partners: Lessons Learned
  • 09:35 Ana Sokolova: Simple Traces for Coalgebras of Composed Monads
  • 10:05 Wolfgang Pree: autoBAHN4mining—autonomously driving mining trains/trucks
  • 10:35 Coffee Break
  • 11:00 Keynote Martina Seidl: Never trust your solver: Certificates for SAT and QBF
  • 11:45 Robert Elsässer: Recent Results on Fast Plurality Consensus
  • 12:15 Lunch Break
  • 13:15 Michael Starzinger: Unicorn – Bit-Precise Reasoning for Symbolic Execution and Code Optimization
  • 13:45 Stefan Resmerita: Modeling and simulation in embedded software development


  •  Nikolaus Augsten: Research with Industry Partners: Lessons Learned
    With the broad adoption of process mining techniques in industry, process mining tools now face massive data volumes with process logs that can store hundreds of millions of activities. Process mining queries often require fast response times since the user interacts with a dashboard to gain business insights. To analyze business processes, the so-called traces of the processes are inspected. A trace is a sequence of activities observed in the process log. To facilitate the analysis, similar traces should be grouped into clusters using the well-known DBSCAN algorithm. Unfortunately, current trace clustering approaches do not scale to large collections of traces, neither in terms of runtime nor in terms of memory usage.
    We present a novel technique, TwoL, that was developed in collaboration with an industry partner and solves the scalability issue of the trace clustering problem. TwoL is a new, highly effective similarity index for traces. Compared to previous techniques, TwoL optimizes a cost function to gracefully adapt to different data distributions. With respect to the state of the art in trace clustering, our techniques reduce the memory complexity and achieve speedups of more than an order of magnitude. We reflect on the challenges, opportunities, and insights gained from our research experience with an industry partner.
  •  Robert Elsässer: Recent Results on Fast Plurality Consensus (slides)
    We consider the plurality consensus problem among n agents. Initially, each agent has one of k different opinions. Agents choose random interaction partners and revise their state according to a fixed transition function, depending on their own state and the state of the interaction partners. The goal is to reach a consensus configuration in which all agents agree on the same opinion, and if there is initially a sufficiently large bias towards one opinion, that opinion should prevail.
    We analyze a synchronized variant of the undecided state dynamics defined as follows. The agents act in phases, consisting of a decision and a boosting part. In the decision part, any agent that encounters an agent with a different opinion becomes undecided. In the boosting part, undecided agents adopt the first opinion they encounter.
    We consider this dynamics in the population model and the gossip model. For the population model, our protocol reaches consensus (w.h.p.) in O(log^2 n) parallel time, providing the first polylogarithmic result for k>2 (w.h.p.) in this model. Without any assumption on the bias, fast consensus has only been shown for k=2 for the unsynchronized version of the undecided state dynamics [Clementi et al., MFCS’18]. We show that the synchronized variant of the undecided state dynamics reaches consensus (w.h.p.) in time O(log^2 n), independently of the initial number, bias, or distribution of opinions.
    A simple extension of our protocol in the gossip model yields a dynamics that does not depend on n or k, is anonymous, and has (w.h.p.) runtime O(log^2 n). This solves an open problem formulated by Becchetti et al. [Distributed Computing, 2017].
    This is joint work with Gregor Bankhamer, Petra Berenbrink, Felix Biermeier, Hamed Hosseinpour, Dominik Kaaser, and Peter Kling.
  •  Wolfgang Pree: autoBAHN4mining—autonomously driving mining trains/trucks (slides)
    What we call autoBAHN4mining is a system of autonomously driving trains/trucks, specifically designed for underground environments, with the goal of enhancing safety and significantly reducing driver costs. The system is based on a plug-in architecture that supports a variety of sensor types, such as Lidar and cameras, that can be selected based on the environment and specific requirements. The sensor data processing harnesses deep learning methods and tools. We’ve evaluated methods for effectively finding relevant test-cases that also help in understanding the neural networks at hand. The sensor fusion component manages a world model with a list of observed objects and their positions. Based on the output of the sensor fusion, the behavior component controls the vehicle, depending on the ‘obstacleness’ of an object and the vehicle’s distance from it. Joint work with Felix Hörbinger.
  •  Stefan Resmerita: Modeling and simulation in embedded software development (slides)
  •  Martina Seidl: Never trust your solver: Certificates for SAT and QBF (slides)
    Many formal verification and synthesis approaches rely on advanced reasoning technologies in the background, often in the form of SAT or QBF solvers. Such solvers are sophisticated and highly tuned pieces of software, often too complex to be verified themselves. How can one be sure that the result of such a solver is correct, when it is critical for proving the correctness of another system? If a SAT solver, a tool for deciding a propositional formula, returns satisfiable, then it also returns a model which is easy to check. If the answer is unsatisfiable, the situation is more complicated. And so it is for true and false quantified Boolean formulas (QBFs), which extend propositional logic by quantifiers over the Boolean variables. To increase the trust in a solving result, modern solvers are expected to produce certificates that can independently and efficiently be checked. In this talk, we discuss the state of the art on validating the results of SAT and QBF solvers based on certification.
  •  Ana Sokolova: Simple Traces for Coalgebras of Composed Monads
    Trace semantics for coalgebras has been in the focus of coalgebra theory for the last 15 years. Unlike typical branching-style semantics like bisimilarity, coalgebraic traces are more involved. However, for coalgebras of monads, there is a simple way to define traces: iterate the determinisation, then observe in an algebra of observations. Despite its simplicity this approach to trace semantics covers the more elaborate notions for coalgebras of a monad.
    Monads compose via strong and weak distributive laws. Recent results on this topic, by Cheng and by Goy and Petrisan, enable iterative composition of multiple monads, which we exploit in this work: We show how traces of composed monads relate to traces of “partial determinisations” for the constitutive parts. As a running example we consider transition systems with probabilities, non-determinism, and action labels which are coalgebras of a monad obtained by composing multiple monads, and show e.g. that non-deterministic traces of the belief-state transformer — studied previously for distribution bisimilarity — coincide with traces of the original system. Our results yield a method for iterative (nested) notions of semantics.
    The talk will be gentle introducing softly all necessary notions, taking into account the abstractness of the topic and the breadth of the audience.
  •  Stefan Sprenger: Implementing 3D and AR in Practice: Technical Challenges and Business Considerations **CANCELLED**
    Attendees will gain insights into technical challenges such as hardware limitations, software development, and content creation, as well as business considerations like cost-benefit analysis, target audience, and marketing strategies. By the end of the talk, attendees will have a better understanding of the opportunities and challenges involved in implementing 3D and AR technologies in real-world scenarios.
  •  Michael Starzinger: Unicorn – Bit-Precise Reasoning for Symbolic Execution and Code Optimization (slides)
    In this talk we present Unicorn, a tool for bit-precise reasoning over RISC-V programs for the purpose of code analysis and code optimization. Our tool symbolically encodes all possible bounded program executions, combining both data-flow and control-flow portions of machine code into a single representation akin to SMT/SAT formulae. This allows us to maximize the utilization of existing state-of-the-art SMT/SAT solvers when reasoning over programs. We will give examples that demonstrate how to perform bounded model checking of safety properties in programs with Unicorn. Furthermore we will outline how the same reasoning can be used for code optimization.

Organization Team

  • Anita Bilke
  • Sebastian Forster
  • Daniel Hofer
  • Thomas Hütter
  • Daniel Kocher
  • Adriana Pratter
  • Elisabeth Riedl
  • Ana Sokolova
  • Tijn de Vos