@inproceedings{conchonFMCAD2013,
  author = {Sylvain Conchon and Amit Goel and Sava Krstic and Alain Mebsout and
  Fatiha Zaidi},
  title = {{Invariants for Finite Instances and Beyond}},
  booktitle = {FMCAD},
  year = {2013},
  month = {October},
  address = {Portland, Oregon, USA},
  location = {Portland, Oregon, USA},
  url = {https://www.lri.fr/~mebsout/papers/fmcad2013.pdf},
  abstract = {Verification of safety properties of concurrent programs
                  with an arbitrary numbers of processes is an old
                  challenge. In particular, complex parameterized
                  protocols like FLASH are still out of the scope of
                  state-of-the-art model checkers.  In this paper, we
                  describe a new algorithm, called Brab, that is able
                  to automatically infer invariants strong enough to
                  prove a protocol like FLASH.  Brab computes
                  over-approximations of backward reachable states
                  that are checked to be unreachable in a finite
                  instance of the system. These approximations
                  (candidate invariants) are then model checked
                  together with the original safety
                  properties. Completeness of the approach is ensured
                  by a mechanism for backtracking on spurious traces
                  introduced by too coarse approximations.}
}