Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct (dynamic) program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT): Individual dynamic logics, along with their calculi, are treated as dynamic theories that can be combined to reason about heterogeneous systems whose components are verified using different program logics. HDL provides two key operations: Lifting extends an individual dynamic theory with new program constructs (e.g., the havoc operation or regular programs) and automatically augments its calculus with sound reasoning principles for the new constructs; and Combination enables cross-language reasoning in a single modality via Heterogeneous Dynamic Theories , facilitating the reuse of existing proof infrastructure. By lifting combined theories with regular programs, we obtain heterogeneous control structures that allow us to reason about intertwined cross-language behavior. We formalize dynamic theories, their lifting and combination, and prove the soundness of all proof rules in Isabelle. We also introduce a proof rule combining deductive DL-based reasoning with reasoning principles from Kleene Algebras with Tests. Furthermore, we prove relative completeness theorems for lifting and combination: Under usual assumptions, reasoning about lifted or combined theories is no harder than reasoning about the constituent dynamic theories and their common first-order structure (i.e., the data theory). We demonstrate HDL's value by verifying an automotive case study where a Java controller (formalized in Java dynamic logic) steers a plant model (formalized in differential dynamic logic).

Automated Production Systems (aPS) in regulated industries such as pharmaceuticals, MedTech, or food and beverages must comply with the stringent validation and documentation requirements of Good Manufacturing Practice (GMP) regulations within the European Union (EU). These obligations create significant burdens for aPS manufacturers, particularly when changes require revalidation through manual integration and system testing. But these prerequisites also enable opportunities for lower-effort software verification, leveraging GMP documentation and boundaries of the automation domain to prove, e.g., that an implemented software change realizes the change specification without side effects. This paper proposes a methodical workflow for deriving software slices suitable for formal verification, while being aligned with automation engineering practices and GMP requirements. It defines assumptions for slice utility based on system modularity, interface expressiveness, and domain boundaries. The approach is validated through a real-world GMP-regulated change from a German MedTech aPS manufacturer, following GAMP 5 guidelines, demonstrating the utility for GMP-regulated aPS engineering and automatic verification of a sliced program segment.

Abstract When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To this end, our paper revisits the idea of differential verification which performs reasoning on differences between NNs: On the one hand, our paper proposes a novel abstract domain for differential verification admitting more efficient reasoning about equivalence. On the other hand, we investigate empirically and theoretically which equivalence properties are (not) efficiently solved using differential reasoning. Based on the gained insights, and following a recent line of work on confidence-based verification, we propose a novel equivalence property that is amenable to Differential Verification while providing guarantees for large parts of the input space instead of small-scale guarantees constructed w.r.t. predetermined input points. To this end, we propose an improved approach for (approximately) constraining an NN’s softmax confidence. We implement our approach in a new tool called VeryDiff and perform an extensive evaluation on numerous old and new benchmark families, including new pruned NNs for particle jet classification in the context of CERN’s LHC where we observe median speedups $$>300\times $$ > 300 × over the State-of-the-Art verifier $$\alpha ,\beta $$ α , β -CROWN.

This work presents insights gained by investigating the relationship between algorithmic fairness and the concept of secure information flow. The problem of enforcing secure information flow is well-studied in the context of information security: If secret information may "flow" through an algorithm or program in such a way that it can influence the program’s output, then that is considered insecure information flow as attackers could potentially observe (parts of) the secret. There is a strong correspondence between secure information flow and algorithmic fairness: if protected attributes such as race, gender, or age are treated as secret program inputs, then secure information flow means that these "secret" attributes cannot influence the result of a program. While most research in algorithmic fairness evaluation concentrates on studying the impact of algorithms (often treating the algorithm as a black-box), the concepts derived from information flow can be used both for the analysis of disparate treatment as well as disparate impact w.r.t. a structural causal model. In this paper, we examine the relationship between quantitative as well as qualitative information-flow properties and fairness. Moreover, based on this duality, we derive a new quantitative notion of fairness called fairness spread, which can be easily analyzed using quantitative information flow and which strongly relates to counterfactual fairness. We demonstrate that off-the-shelf tools for information-flow properties can be used in order to formally analyze a program's algorithmic fairness properties, including the new notion of fairness spread as well as established notions such as demographic parity.

Abstract The KeY tool is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable. KeY combines auto-active and fine-grained proof interaction, which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date. The article provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods.

Abstract In this experience report, we present the complete formal verification of a Java implementation of inplace superscalar sample sort ( "Image missing") using the KeY program verification system. As "Image missing" is one of the fastest general purpose sorting algorithms, this is an important step towards a collection of basic toolbox components that are both provably correct and highly efficient. At the same time, it is an important case study of how careful, highly efficient implementations of complicated algorithms can be formally verified directly. We provide an analysis of which features of the KeY system and its verification calculus are instrumental in enabling algorithm verification without any compromise on algorithm efficiency.

Cyber Physical Production Systems (CPPS) operate for a long time and face continuous and incremental changes to follow up varying requirements. Interdisciplinary engineering of CPPS is often subject to delay and cost overrun; and quality control may even fail due to the lack of efficient information exchange between multiple involved actors. We propose to integrate a formal requirement specification approach, namely Generalized Test Tables including tool support, into industrial workflows and present the approach through extended notations of Business Process Model and Notation (BPMN), namely BPMN++*, with the tool-coupling aspect. The suggested tooling enables automation engineers to follow the defined workflow systematically and communicate easier through the formally represented change requirement. The approach is demonstrated by two typical use cases of changing a CPPS’ control software and showing the result by means of an extended BPMN++ model exemplarily.

Ethereum is a platform for deploying smart contracts, which due to their public nature and the financial value of the assets they manage are attractive targets for attacks. With asset management as a main task of smart contracts, access control aspects are naturally part of the application itself, but also of the functions implemented in a smart contract. Therefore, it is desirable to establish the correctness of smart contracts and their access control on application and single-function level through formal methods. However, there is no established methodology of formalising and verifying correctness properties of smart contracts. In this work, we make an attempt in this direction on the basis of a case study. We choose an existing smart contract application which aims to ascertain the integrity of binary files distributed over the Internet by means of decentralised identity management and access control. We formally specify and verify correctness at the level of single functions as well as temporal properties of the overall application. We demonstrate how to use verified low-level correctness properties for showing correctness at the higher level. In addition, we report on our experience with existing verification tools.

Modern large scale technical systems often face iterative changes on their behaviours with the requirement of validated quality which is not easy to achieve completely with traditional testing. Regression verification is a powerful tool for the formal correctness analysis of software-driven systems. By proving that a new revision of the software behaves similarly as the original version of the software, some of the trust that the old software and system had earned during the validation processes or operation histories can be inherited to the new revision. This trust inheritance by the formal analysis relies on a number of implicit assumptions which are not self-evident but easy to miss, and may lead to a false sense of safety induced by a misunderstood regression verification processes. This paper aims at pointing out hidden, implicit assumptions of regression verification in the context of cyber-physical systems by making them explicit using practical examples. The explicit trust inheritance analysis would clarify for the engineers to understand the extent of the trust that regression verification provides and consequently facilitate them to utilize this formal technique for the system validation.

High requirements regarding quality are set for automated production systems (aPS) as malfunctions can harm humans or cause severe financial loss. These malfunctions can be caused by faults in the control software of the aPS or its inability to correctly identify and handle unintended situations and errors in the technical process or hardware behavior. To achieve more dependable control software, software testing and formal verification can be used to find faults in the software, but require to make assumptions about possible situations (inputs) occurring in the aPS during runtime and often only allow the validation of specific cases. Monitoring individual functions within the control software during runtime can help to identify unspecified situations and raise warnings of the uncertainty about the suitability of a reaction. Yet, the design of reliable monitoring functions requires extensive experience and resources. For this reason, we propose a method for generating monitoring functions from available testing and verification specifications initially used for validating a control software function. Through this, it is possible to continuously assess the behavior of individual software functions and to identify and warn about a) violations of the test specification during runtime and b) unintended situations in which correct software behavior was never tested. Thus, the approach can help to assess and improve both the control software and specification quality through observation and behavior assessment far beyond the testing phase by efficiently reusing existing test specifications for runtime monitoring.

With recent trends in manufacturing automation, such as Industry 4.0, control software in automated production systems becomes more and more complex and volatile, complicating and increasing importance of quality assurance. Test tables are a widely used and generally accepted means to intuitively specify test cases for automation software. However, each table only specifies a single software trace, whereas the actual software behavior may cover multiple similar traces not covered by the table. Within this work, we present a generalization concept for test tables allowing for bounded and unbounded repetition of steps, “don't-care” values, as well as calculations with earlier observed values. We provide a verification mechanism for checking conformance of an IEC 61131-3 PLC software with a generalized test table, making use of a state-of-the-art model checker. Our notation is inspired by widely-used paradigms found in spreadsheet applications. By an empirical study with mechanical engineering students, we show that the notation matches user expectations. A real-world example extracted from an industrial automation plant illustrates our approach.

Several tools and approaches for proving non-interference properties for Java and other languages exist. Some of them have a high degree of automation or are even fully automatic, but over approximate the actual information flow, and hence, may produce false positives. Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence, analysis is time-consuming. In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches: We want to use fully automatic analysis as much as possible and only at places in a program where, due to over approximation, the automatic approaches fail, we resort to more precise, but interactive analysis, where the latter involves the verification only of specific functional properties in certain parts of the program, rather than checking more intricate non-interference properties for the whole program. To illustrate the hybrid approach, in a case study we use this approach - along with the fully automatic tool Joana for checking non-interference properties for Java programs and the theorem prover KeY for the verification of Java programs - as well as the CVJ framework proposed by Kuesters, Truderung, and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an e-voting system. The CVJ framework allows one to establish cryptographic indistinguishability properties for Java programs by checking (standard) non-interference properties for such programs.

Regression verification and checking for illicit information flow in programs are probably the two most prominent instances of so-called relational program reasoning. Regression verification is concerned with proving that two programs behave either equally or differently in a formally specified manner; information-flow checking aims to establish that an attacker cannot distinguish executions of a program that vary in a part of the initial state designated as secret. While the theoretical connections between the two problems are well understood, there are also subtle but significant pragmatic differences. This paper reports the results of an experiment to adapt a state-of-the-art deductive information-flow verification system for Java to the problem of regression verification.

Automated production systems are usually driven by Programmable Logic Controllers (PLCs). These systems are long-living and have high requirements for software quality to avoid downtimes, damaged product and harm to personnel. While commissioning multiple systems of similar type, pragmatic adjustments of the software are often necessary, which results in two or more similar variants of initially identical software. For further evolution of the software, an equivalence analysis of the software's behavior is beneficial to merge divergent development branches into a single program version. This paper presents a novel method for regression verification of PLC code, which allows one to prove that two variants of a plant's software behave identically in specified situations, despite being implemented differently. For this, a regression verification method for PLC code was designed, implemented and evaluated. The notion of program equivalence for reactive PLC code is clarified and defined. Core elements of the method are the translation of PLC code into the SMV input language for model checkers, the adaptation of the coupling invariants concept to reactive systems, and the implementation of a toolchain using a model checker. The approach was successfully evaluated using the Pick-and-Place Unit benchmark case study.

Automated machines and plants are operated for some decades and undergo an everlasting evolution during this time. In this paper, we present three related open evolution challenges focusing on software evolution in the domain of automated production systems, i.e. evolution and co-evolution of (interdisciplinary) engineering models and code, quality assurance as well as variant and version management during evolution.

Abstract We present MODL, a Dynamic Logic and a deductive verification calculus for a core Java-like language that includes multi-threading. The calculus is based on symbolic execution. Even though we currently do not handle non-atomic loops, employing the technique of symmetry reduction allows us to verify systems without limits on state space or thread number. We have instantiated our logic for (restricted) multi-threaded Java programs and implemented the verification calculus within the KeY system. We demonstrate our approach by verifying a central method of the StringBuffer class from the Java standard library in the presence of unbounded concurrency.

In this paper, we present an approach aiming at full junctional deductive verification of concurrent Java programs, based on symbolic execution. We define a dynamic logic and a deductive verification calculus for a restricted fragment of Java with native concurrency primitives. Even though we cannot yet deal with non-atomic loops, employing the technique of symmetry reduction allows us to verify unbounded systems. The calculus has been implemented within the KeY system, and we demonstrate it by verifying a central method of the StringBuffer class from the Java standard library.

Formal methods can only gain widespread use in industrial software development if they are integrated into software development techniques, tools, and languages that are used in practice. The objective of this tutorial is to show how formal specification and deductive verification of object-oriented programs can be done within a software development platform that supports contemporary design and implementation methodologies. The KeY System (developed by the tutorial presenters) is used for demonstration purposes, which implements our approach and integrates formal methods into the commercial CASE tool Borland Together Control Center 6.2 and, alternatively, the open extensible IDE Eclipse.

Abstract Refinement is a well-established and accepted technique for the systematic development of correct software systems. However, for the step from already refined specification to implementation, a correct refinement is often not possible because the data types used in the specification respectively the implementation language differ. In this paper, we discuss this problem and its consequences, using the integer data types of Java as an example, which do not correctly refine the mathematical integers ℤ. We present a solution, which can be seen as a generalisation of refinement and a variant of retrenchment. It has successfully been implemented as part of the KeY software verification system.

We propose an extension of the design-by-contract approach. In addition to preconditions, postconditions, and invariants as the basis for proving properties of a program, information is also provided on which parts of the state are not changed by running the program. This is done in the form of modifier sets. We present a precise semantics of modifier sets and theorems on how to use them in program-correctness proofs. This technique has been implemented as part of the KeY system.

This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project 1 , which is aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. The KeY system consists of a commercial CASE tool enhanced with functionality for formal specification and deductive verification. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

. We present the theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, that is called removal of anti-links. Possible applications of anti-links include computation of prime implicates of large non-clausal formulas as required, for example, in diagnosis. Anti-links do not compute any normal form of a given formula themselves, rather, they remove certain forms of redundancy from formulas in negation normal form (NNF). Their main advantage is that no clausal normal form has to be computed in order to remove redundant parts of a formula. In this paper, we define an anti-link operation on a generic language for expressing many-valued logic formulas called signed NNF and we show that all interesting properties of two-valued anti-links generalize to the many-valued setting, although in a non-trivial way. 1 Introduction In this article we present the theoretical foundations of the many-valued generalizati...

This paper tries to identify the basic problems encountered in handling equality in the semantic tableau framework, and to describe the state of the art in solving these problems. The two main paradigms for handling equality are compared: adding new tableau expansion rules and using E-unification algorithms.