Skip to content
Register Sign in Wishlist

Program Logics for Certified Compilers

$89.99 (P)

Andrew W. Appel, Robert Dockins, Aquinas Hobor, Josiah Dodds, Xavier Leroy, Sandrine Blazy, Gordon Stewart, Lennart Beringer
View all contributors
  • Date Published: April 2014
  • availability: Available
  • format: Hardback
  • isbn: 9781107048010

$ 89.99 (P)

Add to cart Add to wishlist

Other available formats:

Looking for an examination copy?

If you are interested in the title for your course we can consider offering an examination copy. To register your interest please contact providing details of the course you are teaching.

Product filter button
About the Authors
  • Separation Logic is the twenty-first-century variant of Hoare Logic that permits verification of pointer-manipulating programs. This book covers practical and theoretical aspects of Separation Logic at a level accessible to beginning graduate students interested in software verification. On the practical side it offers an introduction to verification in Hoare and Separation logics, simple case studies for toy languages, and the Verifiable C program logic for the C programming language. On the theoretical side it presents separation algebras as models of separation logics; step-indexed models of higher-order logical features for higher-order programs; indirection theory for constructing step-indexed separation algebras; tree-shares as models for shared ownership; and the semantic construction (and soundness proof) of Verifiable C. In addition, the book covers several aspects of the CompCert verified C compiler, and its connection to foundationally verified software analysis tools. All constructions and proofs are made rigorous and accessible in the Coq developments of the open-source Verified Software Toolchain.

    • The only book written for students that covers the practical and theoretical aspects of separation logic
    • Explains the free open-source Verified Software Toolchain
    • Breaks new ground in the science of connecting verified software to verified compilers
    • Accompanied by a free 50-page 'Verifiable C' reference manual
    Read more

    Customer reviews

    Not yet reviewed

    Be the first to review

    Review was not posted due to profanity


    , create a review

    (If you're not , sign out)

    Please enter the right captcha value
    Please enter a star rating.
    Your review must be a minimum of 12 words.

    How do you rate this item?


    Product details

    • Date Published: April 2014
    • format: Hardback
    • isbn: 9781107048010
    • length: 472 pages
    • dimensions: 231 x 150 x 25 mm
    • weight: 0.75kg
    • contains: 52 b/w illus.
    • availability: Available
  • Table of Contents

    1. Introduction
    Part I. Generic Separation Logic:
    2. Hoare logic
    3. Separation logic
    4. Soundness of Hoare logic
    5. Mechanized semantic library Andrew W. Appel, Robert Dockins and Aquinas Hobor
    6. Separation algebras
    7. Operators on separation algebras
    8. First-order separation logic
    9. A little case study
    10. Covariant recursive predicates
    11. Share accounting
    Part II. Higher-Order Separation Logic:
    12. Separation logic as a logic
    13. From separation algebras to separation logic
    14. Simplification by rewriting
    15. Introduction to step-indexing
    16. Predicate implication and subtyping
    17. General recursive predicates
    18. Case study: separation logic with first-class functions
    19. Data structures in indirection theory
    20. Applying higher-order separation logic
    21. Lifted separation logics
    Part III. Separation Logic for CompCert:
    22. Verifiable C
    23. Expressions, values, and assertions
    24. The VST separation logic for C light
    25. Typechecking for Verifiable C Josiah Dodds
    26. Derived rules and proof automation for C light
    27. Proof of a program
    28. More C programs
    29. Dependently typed C programs
    30. Concurrent separation logic
    Part IV. Operational Semantics of CompCert:
    31. CompCert
    32. The CompCert memory model Xavier Leroy, Andrew W. Appel, Sandrine Blazy and Gordon Stewart
    33. How to specify a compiler Lennart Beringer, Robert Dockins and Gordon Stewart
    34. C light operational semantics
    Part V. Higher-Order Semantic Models:
    35. Indirection theory Aquinas Hobor, Andrew Appel and Robert Dockins
    36. Case study: lambda-calculus with references
    37. Higher-order Hoare logic
    38. Higher-order separation logic
    39. Semantic models of predicates-in-the-heap
    Part VI. Semantic Model and Soundness of Verifiable C:
    40. Separation algebra for CompCert
    41. Share models
    42. Juicy memories Gordon Stewart and Andrew W. Appel
    43. Modeling the Hoare judgment
    44. Semantic model of CSL
    45. Modular structure of the development
    Part VII. Applications:
    46. Foundational static analysis
    47. Heap theorem prover Gordon Stewart, Lennart Beringer and Andrew W. Appel.

  • Resources for

    Program Logics for Certified Compilers

    Andrew W. Appel

    General Resources

    Find resources associated with this title

    Type Name Unlocked * Format Size

    Showing of

    Back to top

    This title is supported by one or more locked resources. Access to locked resources is granted exclusively by Cambridge University Press to instructors whose faculty status has been verified. To gain access to locked resources, instructors should sign in to or register for a Cambridge user account.

    Please use locked resources responsibly and exercise your professional discretion when choosing how you share these materials with your students. Other instructors may wish to use locked resources for assessment purposes and their usefulness is undermined when the source files (for example, solution manuals or test banks) are shared online or via social networks.

    Supplementary resources are subject to copyright. Instructors are permitted to view, print or download these resources for use in their teaching, but may not change them or use them for commercial gain.

    If you are having problems accessing these resources please contact

  • Author

    Andrew W. Appel, Princeton University, New Jersey
    Andrew W. Appel is the Eugene Higgins Professor and Chairman of the Department of Computer Science at Princeton University, New Jersey, where he has been on the faculty since 1986. His research is in software verification, computer security, programming languages and compilers, automated theorem proving, and technology policy. He is known for his work on Standard ML of New Jersey and on Foundational Proof-Carrying Code. He is a Fellow of the Association for Computing Machinery, recipient of the ACM SIGPLAN Distinguished Service Award, and has served as Editor in Chief of ACM Transactions on Programming Languages and Systems. His previous books include Compiling with Continuations (1992), the Modern Compiler Implementation series (1998 and 2002) and Alan Turing's Systems of Logic (2012).

    With contributions by

    Robert Dockins, Portland State University

    Aquinas Hobor, National University of Singapore

    Lennart Beringer, Princeton University, New Jersey

    Josiah Dodds, Princeton University, New Jersey

    Gordon Stewart, Princeton University, New Jersey

    Sandrine Blazy, Université de Rennes I, France

    Xavier Leroy, Institut National de Recherche en Informatique et en Automatique (INRIA), Rocquencourt


    Andrew W. Appel, Robert Dockins, Aquinas Hobor, Josiah Dodds, Xavier Leroy, Sandrine Blazy, Gordon Stewart, Lennart Beringer

Sign In

Please sign in to access your account


Not already registered? Create an account now. ×

Sorry, this resource is locked

Please register or sign in to request access. If you are having problems accessing these resources please email

Register Sign in
Please note that this file is password protected. You will be asked to input your password on the next screen.

» Proceed

You are now leaving the Cambridge University Press website. Your eBook purchase and download will be completed by our partner Please see the permission section of the catalogue page for details of the print & copy limits on our eBooks.

Continue ×

Continue ×

Continue ×

Find content that relates to you

Join us online

This site uses cookies to improve your experience. Read more Close

Are you sure you want to delete your account?

This cannot be undone.


Thank you for your feedback which will help us improve our service.

If you requested a response, we will make sure to get back to you shortly.

Please fill in the required fields in your feedback submission.