Prelimniary Programme

Keywords: Probabilistic Process Calculi, Encodings, Quantum Based Systems

Machine Learning and Quantum Computing must be recognized as the new technological frontiers, reshaping the landscape of computation across diverse fields. Their unreliable and highly complex nature, however, poses significant challenges regarding their use in practice as it requires rigorous verification to obtain formal guarantees of correctness. In classical software systems, verification was made possible by a series of principles (program decomposition, determinism, etc.) that no longer apply in quantum and ML software. In this paper, we examine similarities between the formal verification of quantum and ML software and identify common research directions. Particularly in the field of ML, there are ongoing research efforts, which we expect to generate synergies that can be exploited in the context of quantum software. We discuss significant overlaps and research opportunities and propose a close collaboration of those two fields in the future.

Stipula is an executable language that formalizes the operational semantics of legal contracts. It combines aspects from state automata, time, asynchronous and imperative programming. We sketch how a large class of Stipula programs can be modeled and formally verified in KeY. This is joint work with Cosimo Laneve (U Bologna) and Adele Veschetti.

Smart contracts, as integral components of blockchain technology, play a pivotal role in automating and executing agreements in a trust free manner. However, ensuring the correctness and reliability of smart contracts remains a significant challenge due to their complex nature and potential vulnerabilities. To address this challenge, we propose SmartML, a novel modeling language tailored specifically to smart contracts. This paper presents an in-depth exploration of the features, advantages, and applications of the proposed modeling language. By providing a precise and intuitive means of describing smart contract behaviors, SmartML aims to support the development, verification, and validation of smart contracts, ultimately bolstering trust and confidence in them. Furthermore, we discuss the relation to our modeling language with existing blockchain technologies and highlight its potential to streamline integration efforts. We posit SmartML as a versatile tool to advance, interoperability, reliability, and security of smart contracts in blockchain ecosystems.

In my talk, I will discuss notions of safety and liveness in the adversarial domain of smart contract applications. I present a specification language for capturing relevant temporal properties in this domain. Furthermore, I discuss verification of these properties in the context of the SCAR smart contract application metamodel.

Solidity, the main programming language for smart contracts in cryptocurrencies, is being formalized in KeY.

One of the main challenges is to modeling data types to it.

These data types are different from Java in some interesting ways.

Programs must be correct with respect to their application domain. Yet, current the program specification and verification approaches only consider correctness in terms of computations.

In this work, we present a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view.

This enables to not only specify the correctness of a program in terms of the domain without referring to the computational details, but also enables to interpret failed proof attempts in the domain.

For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, a recently proposed approach to interpret a program as a knowledge graph.

We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification.

We analyse OpenJDK's BitSet class with a combination of formal specification, testing and preliminary verification. The BitSet class represents a vector of bits that grows as required. During our analysis, we uncovered a number of bugs. We propose and compare various solutions, supported by our formal specification. Until a solution is chosen for the discovered problems, the source code is not (sufficiently) fixed to allow full mechanical verification in KeY of the class. But we do show initial steps taken towards verification, discuss our experience and identify necessary extensions (particularly for bitwise operations) required to make a complete proof possible once the source code is stable.

We show a verified controller that regulates a heat exchange system.

We present the verification of the Norway Election Algorithm using the KeY Tool. We report on the approach and experiences.

This talk introduces sabotage as an additional, simple and natural primitive game action in Parikh’s game logic, which allows players to lay traps for the opponent. This closes the expressiveness gap between game logic and the strictly more expressive modal mu-calculus. This reveals a close connection between the entangled nested recursion inherent in modal fixpoint logics and adversarial dynamic rule changes characteristic for sabotage games. Completeness is transferred from the proof calculus for the mu-calculus via syntactic equiexpressiveness transformations. The completeness of a simple extension of Parikh’s calculus for game logic follows. Applied to differential game logic, these results show that the differential mu-calculus is complete with respect to first-order fixpoint logic and differential game logic is complete with respect to its ODE-free fragment via a fixpoint characterisation of the continuous dynamics.

For 25 years, the KeY tool has been used to verify the correctness of Java programs. We work toward generalizing KeY's approach and its codebase to new languages. The most ambitious such language is Rust, which ensures memory safety without a garbage collector.

We present some compelling problems resulting from extending KeY to a new language, some unique properties of Rust, and their impact on verification.

Refinement type systems allow programmers to use logical conditions to constrain admissible values of variables. However, most practical refinement type systems limit the expressiveness in the logic to remain automatically decidable and easy to use. Deductive verification tools, on the other hand, often come with expressive specification languages and powerful proof calculi that require interaction and scale badly with the program size.

We introduce Kukicha, a refinement type system framework for Java that enables the interoperation of efficient type checking and deductive program verification. Kukicha combines refinement types with uniqueness types to track aliasing and packing types to track temporary violations. The use of a packing mechanism in combination with deductive verification allows Kukicha to be more expressive than similar type systems. Kukicha first performs an efficient syntactic well-typedness check. If this does not succeed, it emits a translated program where type annotations are replaced JML by specifications that can be proven in KeY.

This is a short talk on enhancing the trustworthiness of automated reasoning tools by building so-called certifying algorithms and corresponding proof checking workflows. I will give a demo based on SAT solving, where the generation and checking of unsatisfiability proof has become a (near) mandatory feature for all modern solvers.

Formal verification of cyber-physical systems is one way to guarantee safety. However, care must be taken because modelling errors might result in proving a faulty controller safe, which is potentially catastrophic in practice. We deal with two such modelling errors in differential dynamic logic, and provide conditions under which these two modelling errors cannot cause a faulty controller to be proven safe. We also show how these conditions can be proven with help of KeYmaera X.

This talk presents an approach for synthesizing provably correct control envelopes for hybrid systems. Control envelopes characterize families of safe controllers and are used to monitor untrusted controllers at runtime. Our algorithm fills in the blanks of a hybrid system's sketch specifying the desired shape of the control envelope, the possible control actions, and the system's differential equations. In order to maximize the flexibility of the control envelope, the synthesized conditions saying which control action can be chosen when should be as permissive as possible while establishing a desired safety condition from the available assumptions, which are augmented if needed. An implicit, optimal solution to this synthesis problem is characterized using hybrid systems game theory, from which explicit solutions can be derived via symbolic execution and sound, systematic game refinements. Ideas for generalization to a broad class of envelope sketches, characterized by admitting a natural representation in differential game logic are presented. The resulting algorithm is demonstrated in a range of safe control envelope synthesis examples with different control challenges.

This talk introduces differential hybrid games, which combine differential games with hybrid games. In both kinds of games, two players interact with continuous dynamics. The difference is that hybrid games also provide all the features of hybrid systems and discrete games, but only deterministic differential equations. Differential games, instead, provide differential equations with input by both players, but not the luxury of hybrid games, such as mode switches and discrete or alternating interaction. This talk augments differential game logic with modalities for the combined dynamics of differential hybrid games. It shows how hybrid games subsume differential games and introduces differential game invariants and differential game variants for proving properties of differential games inductively.

We prove the completeness of an axiomatization for initial value problems (IVPs) with compact initial conditions and compact time horizons for bounded open safety, open liveness and existence properties. This result is achieved via a computable procedure that generates symbolic proofs with differential invariants for rigorous error bounds of numerical solutions to such IVPs, bringing insights from symbolic logic and numerical analysis. As the axiomatization is a subset of the implemented axioms in Keymaera X, this also provides a theoretical justification for the verification power of Keymaera X.

We introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneously reason about properties of and relations between hybrid systems. Refinements are useful e.g. for simplifying proofs by relating a concrete hybrid system to an abstract one from which the property can be proved more easily. Uniform substitution is the key to parsimonious prover microkernels. It enables the verbatim use of single axiom formulas instead of axiom schemata with soundness-critical side conditions scattered across the proof calculus. The uniform substitution rule can then be used to instantiate all axioms soundly. Access to differential variables in dRL enables more control over the notion of refinement, which is shown to be decidable on a fragment of hybrid programs.

Models are abstractions used to precisely represent specific aspects of a system in order to make work easier for engineers. This separation of concerns naturally leads to a proliferation of models, and thus to the challenge of ensuring that all models actually represent the same system. We can study this problem by considering that the property is abstracted as a relation between models called consistency. Yet, the exact nature of this relation remains unclear in the context of cyber-physical systems, as such models are heterogeneous and may not be formally described.

Therefore, we propose a formal foundation for consistency relations, by (1) item providing a set-theoretical description of the virtual single underlying model (V-SUM) methodology, (2) relating consistency to model transformations, and (3) studying the connection between consistency of models and their semantics. In particular, we show that a relation on the semantic space of models can be reflected as a relation on models and that this semantics forms a lattice, such that a canonical semantics can be derived from a consistency relation. Our findings lay the foundation for a formal reasoning about precise notions of consistency.

More than 15 years ago, a paper ""Better bug reporting with better privacy"" solved the two problems of automatic bug reports: Specifically, memory dumps might not be sufficient to reconstruct an issue/crash while leaking private information. However, their approach of generating new input-data had limited applicability.

Our tool instruments the source code to record (with low overhead) a compressed control flow trace, which can be directly added to a bug-report (instead of input-data or memory dumps). The trace format is designed to be adaptable to different programming languages.

In the second part, these traces are used not only by visualizing the control-flow in the code: On the developers side, we can debug a trace using symbolic execution (we call that retracing). Our current implementation works on top of either KeY, CBMC or angr.

We also see how to record a trace with KeY and how to restrict symbolic execution (or a part of it) to a single control flow, to avoid loop invariants and path explosion.

Formal software verification relies on properties of functions and built-in operators. Unless these properties are handled directly by decision procedures, an automated verifier includes them in verification conditions by supplying them as universally quantified axioms or theorems. The use of quantifiers sometimes leads to bad performance, especially if automation causes the quantifiers to be instantiated many times.

In this presentation, I will talk about free facts as an alternative to some axioms. A free fact is a pre-instantiated axiom that is generated alongside the formulas in a verification condition that can benefit from the facts. Replacing an axiom with free facts thus reduces the number of quantifiers in verification conditions. Free facts are statically triggered by syntactic occurrences of certain patterns in the proof terms. This is less powerful than the dynamically triggered patterns used during proof construction. However, we found that free facts perform well in practice.

Finite-precision programs inevitably introduce numerical uncertainties due to input noises and finite-precision (roundoff) errors inherent in arithmetic operations. Furthermore, implementing these programs on hardware necessitates a trade-off between accuracy and efficiency. Therefore, it is crucial to ensure that numerical uncertainties remain acceptably small and to optimize implementations for accurate results tailored to specific applications.

Existing analysis and optimization techniques for finite-precision often face challenges related to scalability and applicability in real-world scenarios. In this talk, I will provide a brief overview of my PhD research, which aimed to develop methods for handling input uncertainties and improving the scalability of the state-of-the-art, thus broadening their scope for practical applications.

We developed a program logic and a sequent calculus to formally address the data dependence analysis problem in high-performance computing. This program logic is rich and powerful enough to be used in different contexts when the problem at hand can be formulated in terms of data dependences. In this presentation, we briefly discuss such problems (e.g., method contract generation, noninterference verification, branch prediction, etc.).

Electricity is a vital infrastructural need for all. Reducing energy consumption would benefit economics, sustainability, and the environment in today's climate. However, to reduce consumption, one must know what one consumes. Therefore, we have developed a novel energy profiling system for Java applications. The profiler's basis is on measurements of iterative execution of small segments of Java code. We will then employ both a Bayesian and a summative estimation model to compare the accuracy of their estimates. Note that this is an ongoing paper. Hence, no results are yet available.

In recent years, research in the field of artificial intelligence has made great progress. AI-tools are getting better in simulating human reasoning and behaviour every day. In this paper, we discuss the extent to which AI-tools can support Correctness-by-Construction engineering. This is an approach of formal methods to developing functionally correct programs incrementally on the basis of a formal specification. Using sound refinement rules, the correctness of the constructed program can already be guaranteed in the development process. We analyze the Correctness-by-Construction process regarding steps for potential AI-tool support in the tool CorC, which implements Correctness-by-Construction. We classify the findings in five areas of interest. Based on existing work, expert knowledge, and prototypical experiments, we discuss for each of the areas whether and to what extent AI-tools can support Correctness-by-Construction software development. We address the risk of AI-tools in formal methods and present our vision of AI-integration in the tool CorC to support developers in constructing programs using Correctness-by-Construction engineering.

We investigate how combinations of Large Language Models (LLMs) and symbolic analyses can be used to synthesise specifications of C programs. The LLM prompts are augmented with outputs from two formal methods tools in the Frama-C ecosystem, Pathcrawler and EVA, to produce C program annotations in the specification language ACSL. We demonstrate how the addition of symbolic analysis to the workflow impacts the quality of annotations: information about input/output examples from Pathcrawler produce more context-aware annotations, while the inclusion of EVA reports yields annotations more attuned to runtime errors. In addition, we show that the method infers rather the programs intent than its behaviour, by generating specifications for buggy programs and observing robustness of the result against bugs.

Large Language Models have proved surprisingly effective at solving a wide range of tasks from just a handful of examples. However, their lack of reliability limits their capacity to tackle large problems that require many steps of reasoning. In response, researchers have proposed advanced pipelines that leverage domain-specific knowledge to chain smaller prompts, provide intermediate feedback and improve performance through search. However, the current complexity of writing, debugging, tuning and maintaining such pipelines has put a bound on their sophistication.

We propose a new paradigm for programming with LLMs called oracular programming. In this paradigm, domain experts are invited to define high-level problem-solving strategies as nondeterministic programs. Such programs are reified into infinite search trees for LLM oracles to navigate. A separate demonstration language allows annotating choice points with examples, while keeping them grounded and synchronized as the associated program evolves.

In this talk, we motivate and explain the key concepts of oracular programming. We introduce Delphyne, a framework for oracular programming based on Python, and discuss the associated tooling. We demonstrate our prototype on a preliminary invariant-synthesis case study. We hope that our proposed framework can foster research on intersymbolic AI and facilitate creative combinations of LLMs with symbolic provers.

Recent investigations hint at the ability of large language models (LLMs) to generate formal specifications for given program code. We present preliminary quantitative experiments on the capabilities of LLMs to generate correct specifications. To this end, we use a prototypical integration of GPT (versions 3.5 and 4o) with the deductive program verifier KeY and the bounded model checker JJBMC. We evaluated our prototype on a set of Java programs that are partially annotated with specifications written in the Java Modeling Language (JML). We show that GPT 4o generates correct annotations in approximately half of all instances across the investigated scenarios. For the case of faulty specifications, we investigate how a feed-back loop can help to improve the original answer. Finally, we present a vision of how Large Language Models may support rigorous formal verification of software systems and describe the necessary next steps in this direction.

Can be reduced to short talk if necessary

Guarantees of correctness of programs are becoming more and more important nowadays. KeY is one tool, which can be used to prove the formal correctness of Java programs. It uses syntactic rewriting rules, called taclets, to successively simplify proofs. These taclet rules can be applied by an automated proving mode in KeY. Because the automation can be insufficient for closing some proofs and because proofs can contain thousands of rule applications, it is desirable to provide stronger automated tools to the user. One such tool is the Satisfiablity Modulo Theories (SMT) translation of KeY, which allows the use of SMT provers to close proofs. The SMT translation also lacks the required rules or proving strength for some proofs. It is thus still desirable to improve the already present automated toolset of KeY users.

This work designs a translation of KeY proofs to the higher-order logic prover Isabelle/HOL. In addition to designing this translation this work also shows that the translation can be automated and integrated within KeY by implementing it as a GUI-Extension of KeY.

This work tests the developed Isabelle translation on over 2 400 example proof obligations of KeY. In doing so the Isabelle translation has been found to offer some advantages over the SMT translation and the KeY automation. Although the Isabelle translation does not manage to close all proofs the KeY automation or SMT translation could close, it is able to close proofs, which the KeY automation or the SMT translation could not close.

Thus the Isabelle translation expands the KeY user’s automated toolset in a meaningful way, while also building a foundation for using Isabelle in ways outside automated proof solving in KeY.

Online elections are especially vulnerable to external and internal threats compromising the privacy and integrity of the election. Thus, a voting system for online elections should enable the detection and correction of any errors in the election result — a property called strong software independence.

This can be achieved by risk-limiting audits, which however require adapting traditional privacy requirements for online elections so that sufficient evidence for the audits is produced.

In this talk, I present on-going work on the formalization and verification of secret and end-to-end-verifiable online elections that fulfill the traceability property necessary for post-election, risk-limiting audits, using the Tamarin prover.

Verification of neural networks is essential for their deployment in

safety-critical applications. While most verification approaches target

ReLU networks, the activation functions used in Long Short-Term Memory

(LSTM) networks, crucial for sequence and time series data, still pose

significant challenges.

Existing approaches for verification of LSTMs neglect dependencies

between input variables, when computing linear relaxations of their

activation functions.

In this talk, I am going to present ongoing work for enhancing the

precision of the linear relaxations by leveraging zonotopes to capture

such input dependencies.

The novel framework of Heterogeneous Dynamic Logic presented in this talk allows the systematic combination of multiple program reasoning theories in dynamic logic, similar to the framework of satisfiability modulo theories (SMT) that allows the systematic combination of multiple theories in first-order logic.

Just like the foundation behind SMT are the conditions under which first-order theory combinations preserve decidability, the foundation here are the conditions under which program theory combinations preserve relative completeness.

The resulting combination principles are useful because they make it possible to modularly combine program reasoning on different levels and with different foci:

While preserving a clear separation of concerns between theories, we nonetheless enable a strong combination of insights across theories.