3 ms·
Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust
by malisper 2mo ago
Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of
[0] https://github.com/model-checking/kani https://github.com/model-checking/kani
[1] https://model-checking.github.io/cbmc-training/cbmc/overview/goto-programs.html https://model-checking.github.io/cbmc-training/cbmc/overview...
- touisteur 2mo agoGOTO is back ! So glad to see CBMC used. I used to write translators to GOTO for simple code checking and was wondering where the recent state of the art was. Thanks for the pointers. Did you have a look at why3 and generating verification conditions from Rust or C code (as frama-c does) ?