Verify programs with loops

[pirapira]

The current approaches do not work for programs that contain loops. For verifying programs with loops we need

1. a framework that composes Hoare triples
2. the rule for loops in that Hoare logic
3. proof of soundness of the Hoare logic with respect to the operational semantics
4. an example verification of a program with loops

[pirapira]

This one looks relevant https://www.cs.princeton.edu/~appel/papers/controllogic.pdf but I still need to think how to deal with jumps into dynamically determined locations.

Maybe we can accumulate "if we reach this label with this condition, we are fine" conditions in many places, until we reach the entrypoint of the whole program with a good enough condition.

[pirapira]

The natural continuation of the current efforts would lead somewhere close to http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-114.pdf

[pirapira]

Or Myreen's decompilation of machine code to functional programs.

[pirapira]

Maybe first I try to verify a simple program with loops by brute-force, run into problems, and use the above ideas.