Skip to content

Bitwalker: Formal Specification and Verification of Poke

Open
No due date
Last updated Sep 10, 2014
100% complete
  • write an ACSL-contract for Bitwalker_Poke
  • find reusable predicates, logic functions and lemmas for example for bit manipulations
  • try to verify Bitwalker_Poke 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

    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.