[Why3-club] Low level constructs

Claude Marché Claude.Marche at inria.fr
Tue Aug 23 13:31:22 CEST 2016

Le 15/08/2016 à 21:01, Jean-Christophe Filliatre a écrit :
> The ARM paper mentioned by Per builds upon an older paper of mine where
> the verification of assembly programs is considered. You can find it
> here: http://www.lri.fr/~filliatr/publis/verifmix.pdf
> This handles arbitrary control flows, provided any loop in the CFG
> contains at least an invariant.

Just to add my 2 cents: the same idea for handling arbitrary control
flow is reused in the following thesis (Section 9.5 in particular)


to deal with x86 assembly code.

- Claude

Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |

More information about the Why3-club mailing list