3 papers
cs.PL2026
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…
cs.DB2026
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…
cs.LO2026
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),…