Mostly sound type system improves a foundational program verifier

Author(s): Dodds, J; Appel, Andrew W.

Download

To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1hw2k

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. © Springer International Publishing 2013.
Publication Date:	1-Dec-2013
Citation:	Dodds, J, Appel, AW. "Mostly sound type system improves a foundational program verifier" Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8307 LNCS, 17 - 32, doi:10.1007/978-3-319-03545-1_2
DOI:	doi:10.1007/978-3-319-03545-1_2
ISSN:	0302-9743
EISSN:	1611-3349
Pages:	17 - 32
Type of Material:	Conference Article
Series/Report no.:	Lecture Notes in Computer Science;
Journal/Proceeding Title:	Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013
Version:	This is the author’s final manuscript. All rights reserved to author(s).