Theories

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