Verified Erasure Correction in Coq with MathComp and VST
Authors: Joshua M. Cohen, Qinshi Wang and Andrew W. Appel
Paper Information
| Title: | Verified Erasure Correction in Coq with MathComp and VST |
| Authors: | Joshua M. Cohen, Qinshi Wang and Andrew W. Appel |
| Proceedings: | CAV 2022 All Papers |
| Editors: | Yakir Vizel, Sharon Shoham and Hari Govind Vediramana Krishnan |
| Keywords: | Reed-Solomon coding, Functional correctness verification, Interactive theorem proving |
| Pages: | 21 |
| Talk: | Aug 09 15:00 (Session 104A: Deductive Verification and Decision Procedures) |
| Paper: |  |