Describir: Vol. 4171 Verified Software: Theories, Tools, Experiments :