Automating Regression Verification of Pointer Programs by Predicate Abstraction (bibtex)
by Vladimir Klebanov, Philipp Rümmer and Mattias Ulbrich
Abstract:
Regression verification is an approach complementing regression testing with formal verification. The goal is to formally prove that two versions of a program behave either equally or differently in a precisely specified way. In this paper, we present a novel automated approach for regression verification that reduces the equivalence of two related imperative pointer programs to constrained Horn clauses over uninterpreted predicates. Subsequently, state-of-the-art SMT solvers are used to solve the clauses. We have implemented the approach, and our experiments show that non-trivial programs with integer and pointer arithmetic can now be proved equivalent without further user input.
Reference:
Automating Regression Verification of Pointer Programs by Predicate Abstraction (Vladimir Klebanov, Philipp Rümmer and Mattias Ulbrich), In Formal Methods in System Design, Springer, volume 52, 2018.
Bibtex Entry:
@Article{KlebanovRuemmerUlbrich2017,
  title        = {Automating Regression Verification of Pointer
                  Programs by Predicate Abstraction},
  doi          = {10.1007/s10703-017-0293-8},
  author       = {Vladimir Klebanov and Philipp R{\"u}mmer and Mattias
                  Ulbrich},
  publisher    = {Springer},
  journal      = {Formal Methods in System Design},
  year         = {2018},
  month        = jun,
  volume       = 52,
  number       = 3,
  pages        = {229--259},
  issn         = {1572-8102},
  doi          = {10.1007/s10703-017-0293-8},
  http         =
                  {https://formal.iti.kit.edu/biblio/?lang=en&key=KlebanovRuemmerUlbrich2017},
  abstract     = "Regression verification is an approach complementing
                  regression testing with formal verification. The
                  goal is to formally prove that two versions of a
                  program behave either equally or differently in a
                  precisely specified way. In this paper, we present a
                  novel automated approach for regression verification
                  that reduces the equivalence of two related
                  imperative pointer programs to constrained Horn
                  clauses over uninterpreted predicates. Subsequently,
                  state-of-the-art SMT solvers are used to solve the
                  clauses. We have implemented the approach, and our
                  experiments show that non-trivial programs with
                  integer and pointer arithmetic can now be proved
                  equivalent without further user input.",
  keywords     = {IMPROVE},
}
Powered by bibtexbrowser