Talk Title: A Formal Analysis Of Error Detecting Codes Using ACL2 (A Work In Progress) Shilpi Goel September 15, 2011 Abstract. Error detecting codes are used to detect accidental changes to data in networks or storage systems. Hence, besides having trust in their correctness, we should also know their error detecting capabilities so that we can choose an appropriate code based on our needs. For example, a noisy channel warrants the use of a code with a high error detecting capabililty. To these ends, we identify three crucial properties of error detecting codes - we call them Soundness, Completeness and Strength. We model some error detecting codes in ACL2, discuss what it means for them to be sound, complete and robust and then prove these properties. Our goal, in the end, is to construct a general framework that will automate such proofs for error control codes.