Using the coq theorem prover to verify complex data structure invariants.

Kenneth Roe, Scott F. Smith

Browse the full MEMOCODE paper archive.