Liquid types in Ada and SPARK... about liquid-rust HOT 3 OPEN

Thank you @rod-chapman for these references! How did you find this project, I almost abandoned it since faced troubles with precise handling branching and loops, could you suggest me what can I read about how to infer loop invariants (if it is possible at all)?

from liquid-rust.

The project was brought to my attention by Alastair Reid at Google Research. He has been keeping close track of projects doing verification with Rust.

Inference of loop invariants is still a hard problem. I know of a few teams that have tried it, but I don't know of any significant success.

from liquid-rust.

An incomplete but useful thing to consider for loop invariants is to use a 'guess and check' approach where you first guess a possible invariant and then use SMT to check whether it holds.

This paper describes an approach (that I have not personally tried) where the guessing part works like this:

1. Gathering some data from an actual run. Which might result in x,y pairs such as 1,3 2,6 3,9.
2. Using linear algebra to produce a guessed invariant "y = 3 * x"

This looks so simple that I keep hoping for an excuse to implement it myself.
There may be more recent papers with improvements - worth doing at least a shallow search if you think this is promising.

from liquid-rust.