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
@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
@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
@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
@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
@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
@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
=> More informations about this toot | More toots from pervognsen@mastodon.social
@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
@zwarich @tmyklebu Yeah, the main dev seems to have completed the AWS Rust std verification challenge for LinkedList with it: https://github.com/verifast/verifast/blob/master/tests/rust/safe_abstraction/linked_list.rs. I gotta say the proof code is a little daunting at a glance. :)
=> More informations about this toot | More toots from pervognsen@mastodon.social
@pervognsen @tmyklebu Wow, that's pretty rough going. As per the Dafny support, I'm curious if you could find the right combination of syntax sugar and automation to not actually require a separate tactic language for practical SW verification usage.
=> More informations about this toot | More toots from zwarich@hachyderm.io
@zwarich @tmyklebu Yeah, I've been playing with Dafny the last few days and the way you implicitly guide the ATP along feels pretty different, a bit more like a paper proof where it's your job to mention the relevant properties and lemmas but you don't have to be super specific about how to apply them. The IDE experience with VS Code is very clean, I recommend checking it out and maybe picking up the book Program Proofs by the main developer if you want something to work through.
=> More informations about this toot | More toots from pervognsen@mastodon.social
@zwarich @tmyklebu The main downside compared to something like Coq or Lean is that failures are a lot more non-informative unless you've already subdivided your proof obligation into small enough pieces that the mere failure to prove a piece gives a strong indication of what went wrong/what is missing. Dunno how much of that could be improved given the relatively black box nature of ATPs.
=> More informations about this toot | More toots from pervognsen@mastodon.social
@pervognsen @zwarich @tmyklebu > black box nature of ATPs.
Why3 has a Coq backend, so you can try to handle the proof by hand :)
=> More informations about this toot | More toots from pkhuong@discuss.systems
text/geminiThis content has been proxied by September (ba2dc).