[HN Gopher] Kani Rust Verifier - a bit-precise model-checker for... ___________________________________________________________________ Kani Rust Verifier - a bit-precise model-checker for Rust Author : pabs3 Score : 39 points Date : 2022-03-24 05:02 UTC (1 days ago) (HTM) web link (model-checking.github.io) (TXT) w3m dump (model-checking.github.io) | Klasiaster wrote: | Nice, I just would have liked to get all these different | verification tools combined under the same interface, just being | different backends as drafted by the rust verification tools work | of project oak: have "cargo verify" as common command and use | common test annotations, allowing the same test to be verified | with different backends or just fuzzed/proptested (see | https://project-oak.github.io/rust-verification-tools/using-... | and https://project-oak.github.io/rust-verification- | tools/using-...). | | The model checking approach seems to be a bit limited regarding | loops. There are also abstract interpreters, such as | https://github.com/facebookexperimental/MIRAI, and symbolic | executers, such as https://github.com/dwrensha/seer or | https://github.com/GaloisInc/crucible. | | Overall I believe this space would benefit from more coordination | and focus on developing something that has the theoretical | foundations to cover as many needs as possible and then make a | user-friendly tool out of it that is endorsed by the Rust project | similar to how Rust analyzer is the one language server to come. ___________________________________________________________________ (page generated 2022-03-25 23:00 UTC)