Verified Erasure Correction in Coq with MathComp and VST
From MaRDI portal
Publication:6487340
DOI10.1007/978-3-031-13188-2_14zbMATH Open1514.68071MaRDI QIDQ6487340FDOQ6487340
Authors: Qinshi Wang, Andrew W. Appel 
Publication date: 7 December 2022
Recommendations
- A library for formalization of linear error-correcting codes
- Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
- Verifying distributed erasure-coded data
- A formal verification method of error correction code processors over Galois-field arithmetic
- Verification, Model Checking, and Abstract Interpretation
Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science) (68P30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Polynomial Codes Over Certain Finite Fields
- Efficient dispersal of information for security, load balancing, and fault tolerance
- Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry
- Title not available (Why is that?)
- Program logics for certified compilers
- A library for formalization of linear error-correcting codes
- Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
- C-language floating-point proofs layered with VST and Flocq
- Connecting higher-order separation logic to a first-order outside world
Cited In (1)
This page was built for publication: Verified Erasure Correction in Coq with MathComp and VST
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6487340)
