@inproceedings{mazur:2008,
  abstract = "Counter abstraction allows us to transform a concurrent system with an unbounded number of agents into a finite-state bounded abstraction, independent of the number of processes present in the implementation. In its general form it is not well suited for verification of parameterised concurrent systems based on message passing that are not fully symmetric and/or use two-way handshaken synchronisation between processes. In this paper we present a method whose main idea is to count processes that are in certain equivalence classes. We use labelled transitions systems to model processes (both implementation and specification) and traces refinement for verification checks. Refinement is checked automatically using the FDR model checker. We illustrate the method on a token ring mutual exclusion algorithm from [P. Wolper and V. Lovinfosse, 1990].",
  author = "Tomasz Mazur",
  booktitle = "Proceedings of the MOdelling and VErifying Process (MOVEP'08)",
  title = "Formal verification of not fully symmetric systems using counter abstraction",
  url = "http://web.comlab.ox.ac.uk/people/tomasz.mazur/publications/tomasz_mazur-movep08-phd.pdf",
  year = "2008",
}


    
      @inproceedings{mazur:2007,
  abstract = "In this paper we consider an adaptation of counter abstraction for the CSP/FDR setting. The technique allows us to transform a concurrent system with an unbounded number of agents into a finite-state abstraction. The systems to which the method can be applied are composed of many identical node processes that run in parallel with a controller process. Refinement checks on the abstract state machine can be performed automatically in the traces and stable failures models using the model checker FDR. We illustrate the method on an example based on a multiprocessor operating system.",
  author = "Tomasz Mazur and Gavin Lowe",
  booktitle = "Proceedings of the Seventh International Workshop on Automated Verification of Critical Systems (AVoCS'07)",
  title = "Counter Abstraction in the CSP/FDR setting",
  url = "http://web.comlab.ox.ac.uk/people/tomasz.mazur/publications/counterabstraction_AVoCS.pdf",
  year = "2007",
}