Ancestors

Written by Per Vognsen on 2024-12-29 at 16:36

I was idly thinking about verification for mutation-based linked structures. A nice thing about bidirectional/doubly-linked structures is that you have an inverse function to work with as opposed to merely an injectivity and surjectivity property, so you don't need a Cantor-Schröder-Bernstein-like argument to pass between the two. More prosaically this also lets you catch functional correctness/memory corruption bugs by checking local invariants like next[prev[x]] = x and prev[next[x]] = x.

=> More informations about this toot | More toots from pervognsen@mastodon.social

Written by tmyklebu on 2024-12-29 at 17:05

@pervognsen Can you do something interesting for verifying reachability invariants? E.g. "Either a node is in the freelist or it's reachable from one of the following roots by following next pointers."

=> More informations about this toot | More toots from tmyklebu@mastodon.gamedev.place

Written by zwarich on 2024-12-29 at 17:48

@tmyklebu @pervognsen As you probably know, transitive closure is inexpressible in first-order logic (a fun exercise with the compactness theorem), and adding it to FOL quickly leads to undecidability. Finding decidable fragments of reachability was once a hot research area, but seems to have died off. Here's one of the last big publications from that line of work: https://csaws.cs.technion.ac.il/~shachari/dl/popl2014.pdf

=> More informations about this toot | More toots from zwarich@hachyderm.io

Written by zwarich on 2024-12-29 at 17:52

@tmyklebu @pervognsen The other more logically satisfactory option is to use monadic second-order logic over tree structures, e.g. https://www.brics.dk/mona/papers/graph-types/article.pdf. Unfortunately, all of the decision procedures for MSOL are automata-based and haven't benefitted from the improvements in SAT solving.

=> More informations about this toot | More toots from zwarich@hachyderm.io

Written by zwarich on 2024-12-29 at 21:29

@tmyklebu @pervognsen Another amusing strategy is to deliberately accept incompleteness and restrict the class of proofs you consider to those that basically just correspond to successive unfolding of definitions:

https://madhu.cs.illinois.edu/pldi13.pdf

I'm curious to know the simplest program/property for which this strategy fails.

=> More informations about this toot | More toots from zwarich@hachyderm.io

Written by zwarich on 2024-12-29 at 21:31

@tmyklebu @pervognsen My slow acceptance of the limitations of this whole line of research is a large part of what made me accept that if there is some widespread usage of program verification, proof assistants will play a role.

=> More informations about this toot | More toots from zwarich@hachyderm.io

Written by Per Vognsen on 2024-12-30 at 04:11

@zwarich @tmyklebu Have you seen the kind of mixed style you can use in Dafny? https://dafny.org/teaching-material/Lectures/2-3-Logic-ProvingByExplaining.html and https://dafny.org/teaching-material/Lectures/2-4-Logic-ProvingByConvincing.html

=> View attached media

=> More informations about this toot | More toots from pervognsen@mastodon.social

Written by zwarich on 2024-12-30 at 05:38

@pervognsen @tmyklebu No, I actually haven't. It seems like a nicer, cleaned up version of VeriFast: https://lirias.kuleuven.be/retrieve/121283/

Also, it seems like VeriFast has been resurrected with Rust support?

https://github.com/verifast/verifast

=> More informations about this toot | More toots from zwarich@hachyderm.io

Toot

Written by Per Vognsen on 2024-12-30 at 09:46

@zwarich Just wrote this example, you can see how relatively low the mark-up burden is for something classical like this.

method Squares(a: array)

modifies a

ensures forall i :: 0 <= i < a.Length ==> a[i] == i * i

{

var jj, djj := 0, 1;

for j := 0 to a.Length

invariant forall i :: 0 <= i < j ==> a[i] == i * i

invariant jj == j * j && djj == 2 * j + 1

{

a[j], jj, djj := jj, jj + djj, djj + 2;

}

}

=> More informations about this toot | More toots from pervognsen@mastodon.social

Descendants