lambda-mountain icon indicating copy to clipboard operation
lambda-mountain copied to clipboard

Published 20 hours ago • verified publisher icon andrew-johnson-4

Coq Proofs TODO LIST

Open andrew-johnson-4 opened this issue 1 year ago • 0 comments

  • [x] check that memory state satisfies a constraint (also expressed as a memory state)
  • parse assertions from gnu assembly
  • yield assertions to Coq proof
  • [x] break Coq proof into basic blocks and transitions
  • validate pre/mid/post-conditions for each basic block

andrew-johnson-4 avatar Aug 23 '24 20:08 andrew-johnson-4