@InProceedings{	  hoang.ea:event-b:2010,
  abstract	= {We present here a case study developing a parallel
		  program. The approach that we use combines refinement
		  and decomposition techniques. This involves in the
		  first step to abstractly specify the aim of the
		  program, then subsequently introduce shared information
		  between sub-processes via refinement. Afterwards,
		  decomposition is applied to split the resulting model into
		  sub-models for different processes. These sub-models are
		  later independently developed using refinement. Our
		  approach aids the understanding of parallel programs and
		  reduces the complexity in their proofs of correctness.},
  author	= {Thai Son Hoang and Jean-Raymond Abrial},
  booktitle	= {Abstract State Machines, Alloy, B and Z (ABZ2010)},
  copyright	= {Springer},
  copyrighturl	= {http://www.springer.com/rights?SGWID=0-122-0-0-0},
  editor	= {Marc Frappier and Uwe Glaesser and Sarfraz Khurshid and
		  Regine Laleau and Steve Reeves},
  language	= {USenglish},
  month		= 2,
  pages		= {319--333},
  publisher	= {Springer},
  series	= {LNCS},
  title		= {Event-B Decomposition for Parallel Programs},
  volume	= 5977,
  year		= 2010,
  user		= {htson}
}