Theories

Buchkapitel

Autor(en):Peter H. Schmitt und Richard Bubel
In:Deductive Software Verification - The KeY Book: From Theory to Practice
Verleger:Springer
Reihe:Lecture Notes in Computer Science
Band:10001
Teil:I: Foundations
Kapitel:5
Jahr:2016
Seiten:149-166
DOI:10.1007/978-3-319-49812-6_5

Abstract

For a program verification tool to be useful it needs to be able to reason about at least the most important data types, both abstract data types, as well as those built into the programming language. This chapter presents how the theories of some data structures are realized in KeY's logic: finite sequences, Java strings, and Java integer data types.

BibTeX

@incollection{SchmittBubel2016,
  author    = {Peter H. Schmitt and Richard Bubel},
  title     = {Theories},
  booktitle = {Deductive Software Verification - The {\KeY} Book: From Theory to Practice},
  series    = {Lecture Notes in Computer Science},
  volume    = {10001},
  pages     = {149--166},
  chapter   = {5},
  part      = {I: Foundations},
  publisher = {Springer},
  year      = {2016},
  doi       = {10.1007/978-3-319-49812-6_5},
  month     = dec,
  abstract  = {For a program verification tool to be useful it needs to
               be able to reason about at least the most important data
               types, both abstract data types, as well as those built
               into the programming language. This chapter presents how
               the theories of some data structures are realized in
               {\KeY}'s logic: finite sequences, {Java} strings, and
               {Java} integer data types.}
}