@TechReport{	  it:2007-014,
  author	= {Parosh Aziz Abdulla and Giorgio Delzanno and Ahmed
		  Rezine},
  title		= {Parameterized Verification of Infinite-state Processes
		  with Global Conditions},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2007},
  number	= {2007-014},
  month		= apr,
  note		= {A short version of this paper will appear in the
		  proceedings of \emph{Computer Aided Verification} (CAV)
		  2007.},
  abstract	= {We present a simple and effective approximated backward
		  reachability algorithm for parameterized systems with
		  existentially and universally quantified global conditions.
		  The individual processes operate on unbounded local
		  variables ranging over the natural numbers. In addition,
		  processes may communicate via broadcast, rendez-vous and
		  shared variables. We apply the algorithm to verify mutual
		  exclusion for complex protocols such as Lamport's bakery
		  algorithm both with and without atomicity conditions, a
		  distributed version of the bakery algorithm, and
		  Ricart-Agrawala's distributed mutual exclusion algorithm.}
}