2 citations · 4 across the 9 of their papers we have counts for
11 papers
A New Interaction Concept for Interactive and Autoactive Program Verification
Wolfram Pfeifer, Mattias Ulbrich, Daniel Drodt
Fully functional program verification is an undecidable$\unicode{x2014}$and, hence, inherently difficult$\unicode{x2014}$task, that is not automatically solvable but typically requ…
Static Type Checking for Database Access Code
Thomas James Kirz, Werner Dietl, Mattias Ulbrich +1
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 d…
Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Samuel Teuber, Mattias Ulbrich, André Platzer +1
Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL),…
Deductive Verification of Floating-Point Java Programs in KeY
Rosa Abbasi Boroujeni, Jonas Schiffl, Eva Darulova +2
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…
Relational Test Tables: A Practical Specification Language for Evolution and Security
Alexander Weigl, Mattias Ulbrich, Suhyun Cha +2
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 informatio…
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
Emanuele De Angelis, Grigory Fedyukovich, Nikos Tzevelekos +1
This volume contains the joint post-proceedings of the 3rd Workshop on Program Equivalence and Relational Reasoning (PERR) and the 6th Workshop on Horn Clauses for Verification and…
Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations
Bernhard Beckert, Timo Bingmann, Moritz Kiefer +3
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-t…
Experience Report: Formal Methods in Material Science
Bernhard Beckert, Britta Nestler, Moritz Kiefer +2
Increased demands in the field of scientific computation require that algorithms be more efficiently implemented. Maintaining correctness in addition to efficiency is a challenge t…
Relational Equivalence Proofs Between Imperative and MapReduce Algorithms
Bernhard Beckert, Timo Bingmann, Moritz Kiefer +3
MapReduce frameworks are widely used for the implementation of distributed algorithms. However, translating imperative algorithms into these frameworks requires significant structu…
A Dual-Engine for Early Analysis of Critical Systems
Aboubakr Achraf El Ghazi, Ulrich Geilmann, Mattias Ulbrich +1
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 wi…
Reducing the Complexity of Quantified Formulas via Variable Elimination
Aboubakr Achraf El Ghazi, Mattias Ulbrich, Mana Taghdiri +1
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…