[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)