Abstract : We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.
https://hal.inria.fr/hal-00967132
Contributor : Claude Marché
<>
Submitted on : Friday, March 28, 2014 - 9:22:17 AM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Saturday, June 28, 2014 - 11:00:42 AM
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Let's Verify This with Why3. Software Tools for Technology Transfer (STTT), Springer, 2015, 17 (6), pp.709-727. ⟨10.1007/s10009-014-0314-5⟩. ⟨hal-00967132⟩
