@InProceedings{PodelskiWies10CounterexampleGuidedFocus,
  author = {Andreas Podelski and Thomas Wies},
  title = {Counterexample-Guided Focus},
  booktitle = {37th ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages, POPL 2010, Madrid,
               Spain, January 20-22, 2010},
  publisher = {ACM},
  year = 2010,
  subproject={S2},
  access={open},
  bibtex={CounterexampleGuidedFocus.bib},
  pdf={CounterexampleGuidedFocus.pdf},
abstract={The automated inference of quantified invariants is considered
one of the next challenges in software verification.  The
question of the right precision-efficiency tradeoff for the
corresponding program analyses here boils down to the question of
the right treatment of disjunction below and above the universal
quantifier.  In the closely related setting of shape analysis one
uses the focus operator in order to adapt the treatment of
disjunction (and thus the efficiency-precision tradeoff) to the
individual program statement.  One promising research direction
is to design parameterized versions of the focus operator which
allow the user to fine-tune the focus operator not only to the
individual program statements but also to the specific
verification task. We carry this research direction one step
further. We fine-tune the focus operator to each individual step
of the analysis (for a specific verification task). This
fine-tuning must be done automatically.  Our idea is to use
counterexamples for this purpose.  We realize this idea in a tool
that automatically infers quantified invariants for the
verification of a variety of heap-manipulating programs.}
}