We introduce a uniform substitution calculus for dLCHP, the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious prover kernels by using axioms instead of axiom schemata. Instantiations can be recovered from a single proof rule responsible for soundness-critical instantiation checks rather than being spread across axiom schemata in side conditions. Even though communication and parallelism reasoning are notorious for necessitating subtle soundness-critical side conditions, uniform substitution when gen- eralized to dLCHP manages to limit and isolate their conceptual overhead. Since uniform substitution has proven to simplify the implementation of hybrid systems provers substantially, uniform substitution for dLCHP paves the way for a parsimonious implementation of theorem provers for hybrid systems with communication and parallelism.

The top-down solver (TD) is a local fixpoint algorithm for arbitrary equation systems. It considers the right-hand sides as black boxes and detects dependencies between unknowns on the fly—features that significantly increase both its usability and practical efficiency. At the same time, the recursive evaluation strategy of the TD, combined with the non-local destabilization mechanism, obfuscates the correctness of the computed solution. To strengthen the confidence in tools relying on the TD as their fixpoint engine, we provide a first machine-checked proof of the partial correctness of the TD. Our proof builds on the observation that the TD can be obtained from a considerably simpler recursive fixpoint algorithm by applying an optimization that neither affects the termination behavior nor the computed result. Accordingly, we break down the proof into a proof of the plain TD, which is only then extended to include the optimization. The backbone of our proof is a mutual induction following the solver’s computation trace. We establish sufficient invariants about the solver state to conclude the correctness of its optimization, i.e., the plain TD terminates if and only if the full TD terminates, and they return the identical assignment. The proof is written using Isabelle/HOL and is available in the archive of formal proofs.

Software verification witnesses are objects containing usefull information to either aid the verification of a Program or identify potential counterexamples. Primarily produced by automatic software verifiers, they can be used to not only confirm or refute verification results, but also for general exchange of information among various tools. This talk will provide an introduction to witnesses and an overview of their current applications.

Computing systems, omnipresent in our daily lives, demand meticulous verification to ensure their correct functionality. Grounded in the foundational theories of logic, automata, and constraint solving, formal methods have been successfully applied in real-world scenarios and delivered correctness guarantees with mathematical rigor. The challenges to formal methods have escalated due to increasing interactions among diverse components, e.g., software programs, hardware circuits, and cyber-physical devices. Therefore, a collaborative and cross-disciplinary approach among traditionally separate research communities is necessary. Although the research communities for formal methods share similar concepts and techniques, their alignment with distinct computational models creates gaps between the communities. In this talk, we will introduce our attempts to bridge the gap between software and hardware analysis, including transferring verification approaches and translating verification tasks. By systematically cross-applying their techniques and extracting valuable insights into analyzing heterogeneous computing systems, we aim to unify verification approaches for comprehensive system-level verification.

Context-sensitive analysis of programs containing recursive procedures may be expensive, in particular, when using expressive domains, rendering the set of possible contexts large or even infinite. Here, we present a general framework for context-sensitivity that allows formalizing not only known approaches such as full-context or call strings but also com binations of these. We propose three generic lifters in this framework to bound the number of encountered contexts on the fly. These lifters are implemented within the abstract interpreter Goblint and compared to existing approaches to context-sensitivity on the SV-COMP benchmark suite. On a subset of recursive benchmarks, all proposed lifters manage to reduce the number of stack-overflows and timeouts compared to a full context approach, with one of them improving the number of correct verdicts by 31% and showing promising results on the considered SV-COMP categories.

In my talk I present recent developments on the tool fm-weck and it's accompanying library fm-actor. Since this SV-COMP a new standard describing formal methods tools (fm-tools) has emerged. The fm-tool yaml aggregates plenty of useful information about each tool and, thanks to SV-COMP, we already have a large database of tools recorded in this new format. With the fm-weck tool I want to make a researchers live easier: many older tools have long been abandoned and require deprecated systems and packages. With fm-weck these tools are conveniently wrapped into a container making them available on modern systems. fm-weck itself build heavily on a new library, fm-actor. With the fm-actor library you can integrate fm-tools into your Python programs with ease.