> Detailanzeige

Batz, Kevin; Chen, Mingshuai; Kaminski, Benjamin Lucien; Katoen, Joost-Pieter; Matheja, Christoph; Schröer, Philipp

Computer Aided Verification: Latticed k-Induction with an Application to Probabilistic Programs

Literatur-
verwaltung

Zur
Merkliste

Lösche von
Merkliste

Per Whatsapp teilen

Schließen

Merkliste



Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
  • Medientyp: E-Artikel
  • Titel: Computer Aided Verification: Latticed k-Induction with an Application to Probabilistic Programs
  • Beteiligte: Batz, Kevin; Chen, Mingshuai; Kaminski, Benjamin Lucien; Katoen, Joost-Pieter; Matheja, Christoph; Schröer, Philipp
  • Erschienen: Springer International Publishing, 2021
  • Erschienen in: Computer Aided Verification (2021), Seite 524-549
  • Sprache: Nicht zu entscheiden
  • DOI: 10.1007/978-3-030-81688-9_25
  • ISSN: 0302-9743; 1611-3349
  • Entstehung:
  • Anmerkungen:
  • Beschreibung: <jats:title>Abstract</jats:title><jats:p>We revisit two well-established verification techniques,<jats:italic>k-induction</jats:italic>and<jats:italic>bounded model checking</jats:italic>(BMC), in the more general setting of fixed point theory over complete lattices. Our main theoretical contribution is<jats:italic>latticed k-induction</jats:italic>, which (i) generalizes classical<jats:italic>k</jats:italic>-induction for verifying transition systems, (ii) generalizes Park induction for bounding fixed points of monotonic maps on complete lattices, and (iii) extends from naturals<jats:italic>k</jats:italic>to transfinite ordinals<jats:inline-formula><jats:alternatives><jats:tex-math>$$\kappa $$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>κ</mml:mi></mml:math></jats:alternatives></jats:inline-formula>, thus yielding<jats:inline-formula><jats:alternatives><jats:tex-math>$$\kappa $$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>κ</mml:mi></mml:math></jats:alternatives></jats:inline-formula><jats:italic>-induction</jats:italic>.</jats:p><jats:p>The lattice-theoretic understanding of<jats:italic>k</jats:italic>-induction and BMC enables us to apply both techniques to the<jats:italic>fully automatic verification of infinite-state probabilistic programs</jats:italic>. Our prototypical implementation manages to automatically verify non-trivial specifications for probabilistic programs taken from the literature that—using existing techniques—cannot be verified without synthesizing a stronger inductive invariant first.</jats:p>