Proof-based Test Case Generation

@incollection{AhrendtGladischEA2016,
  author    = {Wolfgang Ahrendt and
               Christoph Gladisch and
               Mihai Herda},
  title     = {Proof-based Test Case Generation},
  booktitle = {Deductive Software Verification - The {\KeY} Book: From Theory to Practice},
  series    = {Lecture Notes in Computer Science},
  volume    = {10001},
  pages     = {415--451},
  chapter   = {12},
  part      = {III: From Verification to Analysis},
  publisher = {Springer},
  year      = {2016},
  doi       = {10.1007/978-3-319-49812-6_12},
  month     = dec,
  abstract  = {{\KeY}{TestGen} is a white-box test generator for Java methods based on
               {\KeY}'s program analysis and symbolic execution. {\KeY}{TestGen} generates
               a JUnit test harness (test driver) which does not only initialize
               method parameters but also the global state that is defined by the
               (potentially private) fields of objects and classes. For example, a
               complex linked data structure may be created as test input. The
               tests can satisfy different test criteria such as branch coverage,
               path coverage, and MC/DC coverage. The user may also provide a
               specification in the Java Modeling Language (JML) from which a test
               oracle can be generated or which can be used as an abstraction for
               a loop or method call. {\KeY}{TestGen} can be used either as a simple
               stand-alone tool not requiring expert knowledge or it can be used
               in an advanced way to support and complement formal verification.}
}