The Micro_Rust_Examples session contains some explanatory material for working with crush, our weakest-precondition reasoning tactic, and the Micro Rust language, but could do with some more, polished examples. Some suggested verification projects that could serve as nice examples of our framework include:
- In-place sorting of an array, for example via quicksort,
- Manipulating tree data-structures,
- Smaller, more self-contained examples, for example a proof of correctness of an iterative implementation of the Fibonacci function, or similar.
The
Micro_Rust_Examplessession contains some explanatory material for working withcrush, our weakest-precondition reasoning tactic, and the Micro Rust language, but could do with some more, polished examples. Some suggested verification projects that could serve as nice examples of our framework include: