- write an ACSL-contract for Bitwalker_IncrementalWalker_Init, Bitwalker_IncrementalWalker_Peek_Next, Bitwalker_IncrementalWalker_Peek_Finish, Bitwalker_IncrementalWalker_Poke_Next and Bitwalker_IncrementalWalker_Poke_Finish
- specify the type invariants of the struct T_Bitwalker_Incremental_Locals
- specify and verify relations of these functions to each other
- try to verify all functions with automatic theorem provers
- if necessary, verify the rest with an interactive theorem prover
- document strengths and weaknesses of the used tools and specification language
List view
0 issues of 0 selected
There are no open issues in this milestone
Add issues to milestones to help organize your work for a particular release or project. Find and add issues with no milestones in this repo.