Searcharxiv⌕ Search

arXiv subjects

Mattias Ulbrich

Publications and source records attributed to Mattias Ulbrich.

11 recordsLinked to original sources
arXiv2026

A New Interaction Concept for Interactive and Autoactive Program Verification

Fully functional program verification is an undecidable$\unicode{x2014}$and, hence, inherently difficult$\unicode{x2014}$task, that is not automatically solvable but typically requires user interaction and guidance. Existing verifiers either work autoactively, requiring the user to write annotations in source code, without the possibility to inspect the proof state or intervene in case of an unsuccessful attempt, or allow interactions on a logical encoding that is on a lower level than the user-provided specifications. We present a novel interaction concept which allows the user to inspect and interact with the proof state on source code and specification level. This minimizes the mental gap between the representations. We provide an implementation of the concept as a plugin for the Java verification engine KeY, and show with a user study that this prototype can be beneficial for users to understand the proof state and find defects in source code or specifications.

cs.PL↗
arXiv2026

Static Type Checking for Database Access Code

JDBC remains a key technology for database access in Java applications. Since the database dictionary and the Java type system have distinct scopes, developers inevitably need to deal with bugs in SQL-to-Java type mappings. We propose an extension of the Java compiler, based on the established Checker Framework, which allows us to bridge this gap. Our approach verifies statically that the correct Java types are used when setting prepared statement parameters or when getting values from result sets. This allows us to lift a practically important class of runtime errors to compile time. Our approach is sound and, therefore, is guaranteed not to produce false negatives. Our prototype implementation also offers a degraded mode for type-checking legacy software, if developers are only interested in a subset of errors. Our experiments show that our approach detects a wide range of type mismatches in realworld application code and can indeed prevent errors which might otherwise surface as runtime errors. From the perspective of the developer, our approach is extremely lightweight: it processes the unmodified Java code, yet developers may add their own annotations. This allows us to perform type-checking even across method boundaries, whereas commercial developer tools are restricted to local checks. Finally, we show that we can type-check real-world JDBC software with reasonable overhead during compilation.

cs.DB↗
arXiv2025

Heterogeneous Dynamic Logic: Provability Modulo Program Theories

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).

cs.LO↗
arXiv2021

Deductive Verification of Floating-Point Java Programs in KeY

Deductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due to rounding as well as the presence of the special values infinity and `Not a Number' (NaN). In this paper, we present the first floating-point support in a deductive verification tool for the Java programming language. Our support in the KeY verifier handles arithmetic via floating-point decision procedures inside SMT solvers and transcendental functions via axiomatization. We evaluate this integration on new benchmarks, and show that this approach is powerful enough to prove the absence of floating-point special values -- often a prerequisite for further reasoning about numerical computations -- as well as certain functional properties for realistic benchmarks.

cs.PL↗
arXiv2019

Relational Test Tables: A Practical Specification Language for Evolution and Security

A wide range of interesting program properties are intrinsically relational, i.e., they relate two or more program traces. Two prominent relational properties are secure information flow and conditional program equivalence. By showing the absence of illegal information flow, confidentiality and integrity properties can be proved. Equivalence proofs allow using an existing (trusted) software release as specification for new revisions. Currently, the verification of relational properties is hardly accessible to practitioners due to the lack of appropriate relational specification languages. In previous work, we introduced the concept of generalised test tables: a table-based specification language for functional (non-relational) properties of reactive systems. In this paper, we present relational test tables -- a canonical extension of generalised test tables for the specification of relational properties, which refer to two or more program runs or traces. Regression test tables support asynchronous program runs via stuttering. We show the applicability of relational test tables, using them for the specification and verification of two examples from the domain of automated product systems.

cs.LO↗
arXiv2018

Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations

Distributed programs are often formulated in popular functional frameworks like MapReduce, Spark and Thrill, but writing efficient algorithms for such frameworks is usually a non-trivial task. As the costs of running faulty algorithms at scale can be severe, it is highly desirable to verify their correctness. We propose to employ existing imperative reference implementations as specifications for MapReduce implementations. To this end, we present a novel verification approach in which equivalence between an imperative and a MapReduce implementation is established by a series of program transformations. In this paper, we present how the equivalence framework can be used to prove equivalence between an imperative implementation of the PageRank algorithm and its MapReduce variant. The eight individual transformation steps are individually presented and explained.

cs.PL↗
arXiv2018

Experience Report: Formal Methods in Material Science

Increased demands in the field of scientific computation require that algorithms be more efficiently implemented. Maintaining correctness in addition to efficiency is a challenge that software engineers in the field have to face. In this report we share our first impressions and experiences on the applicability of formal methods to such design challenges arising in the development of scientific computation software in the field of material science. We investigated two different algorithms, one for load distribution and one for the computation of convex hulls, and demonstrate how formal methods have been used to discover counterexamples to the correctness of the existing implementations as well as proving the correctness of a revised algorithm. The techniques employed for this include SMT solvers, and automatic and interactive verification tools.

cs.SE↗
arXiv2018

Relational Equivalence Proofs Between Imperative and MapReduce Algorithms

MapReduce frameworks are widely used for the implementation of distributed algorithms. However, translating imperative algorithms into these frameworks requires significant structural changes to the algorithm. As the costs of running faulty algorithms at scale can be severe, it is highly desirable to verify the correctness of the translation, i.e., to prove that the MapReduce version is equivalent to the imperative original. We present a novel approach for proving equivalence between imperative and MapReduce algorithms based on partitioning the equivalence proof into a sequence of equivalence proofs between intermediate programs with smaller differences. Our approach is based on the insight that two kinds of sub-proofs are required: (1) uniform transformations changing the controlflow structure that are mostly independent of the particular context in which they are applied; and (2) context-dependent transformations that are not uniform but that preserve the overall structure and can be proved correct using coupling invariants. We demonstrate the feasibility of our approach by evaluating it on two prototypical algorithms commonly used as examples in MapReduce frameworks: k-means and PageRank. To carry out the proofs, we use the interactive theorem prover Coq with partial proof automation. The results show that our approach and its prototypical implementation based on Coq enables equivalence proofs of non-trivial algorithms and could be automated to a large degree.

cs.LO↗
arXiv2014

Reducing the Complexity of Quantified Formulas via Variable Elimination

We present a general simplification of quantified SMT formulas using variable elimination. The simplification is based on an analysis of the ground terms occurring as arguments in function applications. We use this information to generate a system of set constraints, which is then solved to compute a set of sufficient ground terms for each variable. Universally quantified variables with a finite set of sufficient ground terms can be eliminated by instantiating them with the computed ground terms. The resulting SMT formula contains potentially fewer quantifiers and thus is potentially easier to solve. We describe how a satisfying model of the resulting formula can be modified to satisfy the original formula. Our experiments show that in many cases, this simplification considerably improves the solving time, and our evaluations using Z3 and CVC4 indicate that the idea is not specific to a particular solver, but can be applied in general.

cs.LO↗
arXiv2014

A Dual-Engine for Early Analysis of Critical Systems

This paper presents a framework for modeling, simulating, and checking properties of critical systems based on the Alloy language -- a declarative, first-order, relational logic with a built-in transitive closure operator. The paper introduces a new dual-analysis engine that is capable of providing both counterexamples and proofs. Counterexamples are found fully automatically using an SMT solver, which provides a better support for numerical expressions than the existing Alloy Analyzer. Proofs, however, cannot always be found automatically since the Alloy language is undecidable. Our engine offers an economical approach by first trying to prove properties using a fully-automatic, SMT-based analysis, and switches to an interactive theorem prover only if the first attempt fails. This paper also reports on applying our framework to Microsoft's COM standard and the mark-and-sweep garbage collection algorithm.

cs.LO↗