Mostly sound type system improves a foundational program verifier

Josiah Dodds, Andrew Wilson Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationCertified Programs and Proofs - Third International Conference, CPP 2013, Proceedings
Pages17-32
Number of pages16
DOIs
StatePublished - Dec 1 2013
Event3rd International Conference on Certified Programs and Proofs, CPP 2013 - Melbourne, VIC, Australia
Duration: Dec 11 2013Dec 13 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8307 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other3rd International Conference on Certified Programs and Proofs, CPP 2013
CountryAustralia
CityMelbourne, VIC
Period12/11/1312/13/13

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Mostly sound type system improves a foundational program verifier'. Together they form a unique fingerprint.

  • Cite this

    Dodds, J., & Appel, A. W. (2013). Mostly sound type system improves a foundational program verifier. In Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings (pp. 17-32). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8307 LNCS). https://doi.org/10.1007/978-3-319-03545-1_2