This project is read-only.


Better inference required for loop initialization


In the attached we do not infer a suitable bounds invariant for the innermost loop.

Interestingly, if I try to simplify the kernel even a little bit it does verify. So perhaps we are very close with this one.

file attachments

Closed Feb 23, 2015 at 5:35 PM by jketema
We've been inferring the relevant invariant for a while "LoopBound".


jketema wrote Sep 25, 2014 at 10:57 PM

Are you sure you attached the correct kernel? This one verifies for me.