@InCollection{	  daum.ea:verification:2008,
  abstract	= {Though the verification of operating systems is an active
		  research field, a verification method is still missing that
		  provides both, the proximity to practically used
		  programming languages such as C and a realistic model of
		  concurrency, i.e. a model that copes with the granularity
		  of atomic operations actually used in a target machine.Our
		  approach serves as the foundation for the verification of
		  concurrent programs in C0 – a C fragment enriched by kernel
		  communication primitives – in a Hoare-Logic. C0 is compiled
		  by a verified compiler into assembly code representing a
		  cooperative concurrent transition system. For the latter,
		  it is shown that it can actually be executed in a true
		  concurrent way reflecting the C0 semantics.},
  author	= {Matthias Daum and Jan D\"orrenb\"acher and Mareike Schmidt
		  and Burkhart Wolff},
  booktitle	= {Verified Software: Theories, Tools, Experiments},
  copyright	= {\copyright Springer-Verlag},
  language	= {USenglish},
  month		= {September},
  pages		= {161--176},
  pdf		= {papers/2008/1_libvamos.pdf},
  publisher	= {Springer Berlin / Heidelberg},
  series	= {LNCS 5295},
  title		= {A Verification Approach for System-Level Concurrent
		  Programs },
  url		= {http://www.springerlink.com/content/vl5jk16l93885456/},
  year		= 2008,
  user		= {lukasbru}
}