subject:"\[Why3\-club\] Low level constructs"

Re: [Why3-club] Low level constructs

2016-08-23 Thread Claude Marché

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

Re: [Why3-club] Low level constructs

2016-08-15 Thread Per Lindgren

Hi Neil On 15 Aug 2016, at 17:07, Neil Evans > wrote: Hello, I'm trying to do a comparison between Why3 and MALPAS, specifically WhyML and the MALPAS Intermediate Language (MALPAS IL). (Knowledge of MALPAS is not important for answering my query