@InBook{KlamrothEtAl2022,
author = {Jonas Klamroth and
Florian Lanzinger and
Wolfram Pfeifer and
Mattias Ulbrich},
editor = {Wolfgang Ahrendt and
Bernhard Beckert and
Richard Bubel and
Einar Broch Johnsen},
title = {The Karlsruhe Java Verification Suite},
bookTitle = {The Logic of Software. A Tasting Menu of Formal Methods:
Essays Dedicated to Reiner H{\"a}hnle on the Occasion of
His 60th Birthday},
year = {2022},
month = jul,
publisher = {Springer International Publishing},
pages = {290--312},
isbn = {978-3-031-08166-8},
doi = {10.1007/978-3-031-08166-8\_14},
url = {https://doi.org/10.1007/978-3-031-08166-8_14}
}
The Karlsruhe Java Verification Suite
| Author(s): | Jonas Klamroth, Florian Lanzinger, Wolfram Pfeifer, and Mattias Ulbrich |
|---|---|
| In: | The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday |
| Publisher: | Springer International Publishing |
| Year: | 2022 |
| Pages: | 290-312 |
| Preprint/PDF: | KaJaVe2022.pdf |
| URL: | https://doi.org/10.1007/978-3-031-08166-8_14 |
| DOI: | 10.1007/978-3-031-08166-8_14 |
| Links: | The final publication is available at Springer. |
Abstract
Thanks to the deductive verifier KeY, the formal verification of Java programs has a long-standing tradition at Karlsruhe. The design of KeY implies some properties that can restrict its use in real-world application cases: (1) Verifying long, code-intensive methods with many instructions or bit-wise operations is difficult even if their behaviour is not overly complex, and (2) tracking formal guarantees through unverified code is difficult if not impossible using KeY.