Interval counterexamples for loop invariant learning

Abstract

Loop invariant generation has long been a challenging problem. Black-box learning has recently emerged as a promising method for inferring loop invariants. However, the performance depends heavily on the quality of collected examples. In many cases, only after tens or even hundreds of constraint queries, can a feasible invariant be successfully inferred.

BibTeX

@inproceedings{Xu-al:FSE20,
  author    = {Rongchen Xu and
               Fei He and
               Bow{-}Yaw Wang},
  title     = {Interval counterexamples for loop invariant learning},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {111--122},
  publisher = {{ACM}},
  year      = {2020},
}

Interval counterexamples for loop invariant learning

Abstract

Related papers