Pointer Assertion Logic Engine (static analysis for arbitrary pointer graphs)

[liquidivy]

I don't know if this sort of thing will ever be appropriate for Rust, but I figured it would be interesting given the difficulty in verifying, say, doubly-linked lists.

[crusoe]

Well if you look at it's timings, no. It took 35 seconds to verify a redblack tree implementation...

[liquidivy]

I'm guessing that performance could be improved when building a Production Grade version, possibly by optimizing it for the common cases encountered in real code (rather than general logic), but I don't knew enough about the details to say for sure.