Advertisement
Published in:
2013 | OriginalPaper | Chapter
Mostly Sound Type System Improves a Foundational Program Verifier
Authors : Josiah Dodds, Andrew W. Appel
Published in: Certified Programs and Proofs
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We integrate a verified typechecker with a verified program logic for the C language, proved sound with respect to the operational semantics of the CompCert verified optimizing C compiler. The C language is known to not be type-safe but we show the value of a provably
mostly sound
type system: integrating the typechecker with the program logic makes the logic significantly more usable. The computational nature of our typechecker (within Coq) makes program proof much more efficient. We structure the system so that symbolic execution—even tactical (nonreflective) symbolic execution—can keep the type context and typechecking always in reified form, to avoid expensive re-reification.