2 papers
cs.PL2022
Traits for Correct-by-Construction Programming
Tobias Runge, Alex Potanin, Thomas Thüm +1
We demonstrate that traits are a natural way to support correctness-by-construction (CbC) in an existing programming language in the presence of traditional post-hoc verification (…
cs.PL2018
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
Alexander Knüppel, Thomas Thüm, Carsten Pardylla +1
Deductive verification of software has not yet found its way into industry, as complexity and scalability issues require highly specialized experts. The long-term perspective is, h…