<div dir="ltr"><div style="font-family:tahoma,sans-serif" class="gmail_default">​Hi.</div><div style="font-family:tahoma,sans-serif" class="gmail_default">I understand from [1] (part 4.4) that instruction reordering is verified in vellvm.</div><div style="font-family:tahoma,sans-serif" class="gmail_default">I download vellvm, but I dont know where instruction reordering has considered. And I would like to apply just that to my input.</div><div style="font-family:tahoma,sans-serif" class="gmail_default">Can anyone help me? I am unfamiliar with coq and newbie in formal methods.</div><div style="font-family:tahoma,sans-serif" class="gmail_default"> </div><div style="font-family:tahoma,sans-serif" class="gmail_default">[1] <a href="http://www.cis.upenn.edu/~stevez/papers/ZNMZ12.pdf">http://www.cis.upenn.edu/~stevez/papers/ZNMZ12.pdf</a></div></div>