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 Per Vognsen on 2024-12-29 at 22:42

@zwarich @tmyklebu This reminds me that reachability of states is something you can express in CTL but not in LTL, e.g. the classic resetability property for sequential circuits where you want every state reachable from an initial state to be able to reach a designated reset state.

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

Written by Per Vognsen on 2024-12-29 at 22:45

@zwarich @tmyklebu Although on second thought the situation is not the same for several reasons, e.g in LTL you can't even express that it should be able to reach the reset state in one step, so LTL's shortfall isn't really about the transitive closure: LTL fundamentally doesn't have a way to express the existential path quantifier from CTL.

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

Toot

Written by Per Vognsen on 2024-12-29 at 22:56

@zwarich @tmyklebu Trying to refresh my memory: the Wikipedia page does mention that if you add propositional quantification to CTL (in addition to the path quantification) you get a monadic second-order logic, which I guess intersects with what you were mentioning: https://en.wikipedia.org/wiki/Computation_tree_logic#Relations_with_other_logics

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

Descendants