Verified Erasure Correction in Coq with MathComp and VST

DOI10.1007/978-3-031-13188-2_14MaRDI QIDQ6487340zbMATH OpenFDO

Authors Qinshi Wang, Andrew W. Appel

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Mathematics Subject Classification ID

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)

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

Cites work

• scientific article; zbMATH DE number 1026591 (Why is no real title available?)
• A library for formalization of linear error-correcting codes
• C-language floating-point proofs layered with VST and Flocq
• Connecting higher-order separation logic to a first-order outside world
• Efficient dispersal of information for security, load balancing, and fault tolerance
• Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
• Polynomial Codes Over Certain Finite Fields
• Program logics for certified compilers
• Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry

Cited in

(1)

• A library for formalization of linear error-correcting codes

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)