Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

Theories

Book Chapter

Author(s):Peter H. Schmitt and Richard Bubel
In:Deductive Software Verification - The KeY Book: From Theory to Practice
Publisher:Springer
Series:Lecture Notes in Computer Science
Volume:10001
Part:I: Foundations
Chapter:5
Year:2016
Pages: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.}
}