Update riscv incr example: end-to-end proof

kth-step / HolBA

Binary analysis in HOL

Other

33 stars 20 forks source link

Update riscv incr example: end-to-end proof #176

Closed andreaslindner closed 2 months ago

palmskog commented 2 months ago

@andreaslindner so can I do a small pass on this PR and then approve and merge it? Would be very useful to have some end-to-end proofs as basis, not least when we plan to do a port to the new HOL4.