Skip to main content
SpringerLink
Log in

Mostly Sound Type System Improves a Foundational Program Verifier

  • Conference paper
Certified Programs and Proofs (CPP 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8307))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Appel, A.W.: Tactics for separation logic (2006)

    Google Scholar 

  2. Appel, A.W.: Verified Software Toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1–17. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  3. Appel, A.W.: VeriSmall: Verified Smallfoot shape analysis. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 231–246. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. Cambridge (to appear, 2014)

    Google Scholar 

  5. Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! A framework for higher-order separation logic in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 315–331. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  7. Campbell, B.: An executable semantics for compCert C. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 60–75. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  8. Canet, G., Cuoq, P., Monate, B.: A value analysis for C programs. In: Ninth Source Code Analysis and Manipulation, pp. 123–124. IEEE (2009)

    Google Scholar 

  9. Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI 2011, pp. 234–245 (2011)

    Google Scholar 

  10. Chlipala, A.: Reflection. In: Certified Programming With Dependent Types. MIT Press (2013)

    Google Scholar 

  11. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th Symposium on Principles of Programming Languages (POPL 2012), pp. 533–544. ACM (2012)

    Google Scholar 

  14. Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: Automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 99–115. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  15. Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 578–580 (1969)

    Article  Google Scholar 

  16. Leroy, X.: The CompCert verified compiler, software and commented proof (June 2013), http://compcert.inria.fr

  17. McCreight, A.: Practical tactics for separation logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 343–358. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  18. Norrish, M.: C-to-isabel parser (2013), http://www.ssrg.nicta.com.au/software/TS/c-parser/

  19. Tuerk, T.: A formalisation of Smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469–484. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Princeton University, USA

    Josiah Dodds & Andrew W. Appel

Authors
  1. Josiah Dodds
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrew W. Appel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research Cambridge, 21 Station Road, CB1 2FB, Cambridge, UK

    Georges Gonthier

  2. Canberra Research Lab., NICTA, PO Box 8001, 2601, Canberra, ACT, Australia

    Michael Norrish

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer International Publishing Switzerland

About this paper

Cite this paper

Dodds, J., Appel, A.W. (2013). Mostly Sound Type System Improves a Foundational Program Verifier. In: Gonthier, G., Norrish, M. (eds) Certified Programs and Proofs. CPP 2013. Lecture Notes in Computer Science, vol 8307. Springer, Cham. https://doi.org/10.1007/978-3-319-03545-1_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-03545-1_2

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-03544-4

  • Online ISBN: 978-3-319-03545-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation