Mostly sound type system improves a foundational program verifier

Josiah Dodds; Andrew W. Appel

doi:10.1007/978-3-319-03545-1_2

Mostly sound type system improves a foundational program verifier

Josiah Dodds, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 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 language	English (US)
Title of host publication	Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings
Pages	17-32
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-319-03545-1_2
State	Published - 2013
Event	3rd International Conference on Certified Programs and Proofs, CPP 2013 - Melbourne, VIC, Australia Duration: Dec 11 2013 → Dec 13 2013

Publication series

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

Other

Other	3rd International Conference on Certified Programs and Proofs, CPP 2013
Country/Territory	Australia
City	Melbourne, VIC
Period	12/11/13 → 12/13/13

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-03545-1_2

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

@inproceedings{f475253fcc5b4ffc9ef82710c20a2720,

title = "Mostly sound type system improves a foundational program verifier",

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.",

author = "Josiah Dodds and Appel, {Andrew W.}",

year = "2013",

doi = "10.1007/978-3-319-03545-1_2",

language = "English (US)",

isbn = "9783319035444",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "17--32",

booktitle = "Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings",

note = "3rd International Conference on Certified Programs and Proofs, CPP 2013 ; Conference date: 11-12-2013 Through 13-12-2013",

}

Dodds, J & Appel, AW 2013, Mostly sound type system improves a foundational program verifier. in Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8307 LNCS, pp. 17-32, 3rd International Conference on Certified Programs and Proofs, CPP 2013, Melbourne, VIC, Australia, 12/11/13. https://doi.org/10.1007/978-3-319-03545-1_2

Mostly sound type system improves a foundational program verifier. / Dodds, Josiah; Appel, Andrew W.
Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings. 2013. p. 17-32 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8307 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Mostly sound type system improves a foundational program verifier

AU - Dodds, Josiah

AU - Appel, Andrew W.

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84893057010&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84893057010&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-03545-1_2

DO - 10.1007/978-3-319-03545-1_2

M3 - Conference contribution

AN - SCOPUS:84893057010

SN - 9783319035444

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 17

EP - 32

BT - Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings

T2 - 3rd International Conference on Certified Programs and Proofs, CPP 2013

Y2 - 11 December 2013 through 13 December 2013

ER -

Mostly sound type system improves a foundational program verifier

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this