3 ms·
This is achieved by latching on to rustc, and then compiling to gotoc, which is then used with CBMC. Removed due to my misunderstanding: ~~I don't think Kani
by PartiallyTyped 2y ago
This is achieved by latching on to rustc, and then compiling to gotoc, which is then used with CBMC.
Removed due to my misunderstanding:
~~I don't think Kani counts as a "formal" verification tool, emphasis on "formal", but it is a verification tool for rust code and is powered by CBMC.~~
- IshKebab 2y agoI'm not sure what you're implying. Kani absolutely is formal verification. CBMC stands for C Bounded Model Checker and model checking is one of the main forms of formal verification.
- PartiallyTyped 2y agoEdit: Seems like I misread the documentation... ~~What I was implying is that Kani just can't figure out all of the paths;~~ ~~Consider this example from Kani documentation [1]:~~ fn estimate_size(x: u32) -> u32 { if x < 256 { if x < 128 { return 1; } else { return 3; } } else if x < 1024 { if x > 1022 { panic!("Oh no, a failing corner case!"); } else { return 5; } } else { if x < 2048 { return 7; } else { return 9; } } } ~~Kani is very unlikely to find x=1023.~~ https://model-checking.github.io/kani/tutorial-first-steps.html https://model-checking.github.io/kani/tutorial-first-steps.h...
- accelbred 2y agoKani will find 1023 unless you constrain the input. The link you posted is saying a property test is unlikely to find it but Kani will find it.
- IshKebab 2y agoYeah you misread that. Read it again, it's saying normal fuzzing is unlikely to find it but Kani finds it instantly.
- PartiallyTyped 2y agoOh this is embarrassing.