C. Belo Lourenço, S.-M. Lamraoui, S. Nakajima, and J. Sousa Pinto, “Studying Verification Conditions for Imperative Programs”, eceasst, vol. 72, Nov. 2015.