The Karlsruhe Java Verification Suite

Buchkapitel

Autor(en):Jonas Klamroth, Florian Lanzinger, Wolfram Pfeifer und 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
Verleger:Springer International Publishing
Jahr:2022
Seiten: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:

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.

BibTeX

@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}
}