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) https://tel.archives-ouvertes.fr/tel-00710193 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 | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
