Automatic Verification of Parameterized Linear Networks of Processes

Abstract:
This paper describes a method to verify safety properties of parameterized linear networks of processes. The method is based on the construction of a network invariant, defined as a fixpoint. Such invariants can often be automatically computed using heuristics based on Cousot's widening techniques. These techniques have been implemented and some non-trivial examples are presented.

Reference:

  @INPROCEEDINGS{lesens:popl97,
  AUTHOR = {D. Lesens and N. Halbwachs and P. Raymond},
  TITLE={Automatic Verification of Parameterized
         Linear Networks of Processes},
  BOOKTITLE={24th ACM Symposium on Principles of
             Programming Languages, POPL'97},
  ADDRESS={Paris},
  MONTH={January},
  YEAR= 1997

Postscript file