@TechReport{	  hoang:how:2010,
  abstract	= {In formal reasoning, modelling and proving activities are
		  closely related.Models give rise to different proof
		  obligations and information about failedproofs gives
		  indications on how models should be improved. This document
		  isan attempt to address the latter issue: to understand how
		  to deal with unprovable obligations. We consider here proof
		  obligations related to invariant preservation of an Event-B
		  model: firstly, to understand the meaning of the proof
		  obligations; secondly, to analyse various ways to fix the
		  model accordingly. Our analysis is based on the concept of
		  reachable states and inductive invariants.},
  author	= {Thai Son Hoang},
  institution	= {Department of Computer Science, ETH Zurich},
  language	= {UKenglish},
  month		= 4,
  number	= 672,
  title		= {How to interpret Failed Proofs in Event-B},
  url		= {http://www.inf.ethz.ch/research/disstechreps/techreports},
  year		= 2010,
  user		= {htson}
}