Program Logics for Certified Compilers

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