Moocable is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

Software Foundation Volume 6: Separation Logic Foundations

via University of Pennsylvania

Description

This electronic book is Volume 6 of the Software Foundations series, which presents the mathematical underpinnings of reliable software.

*COMPANION COURSE NOTES*: A large part of this course is also written up in traditional LaTeX-style presentation. It's available from http://www.chargueraud.org/teach/verif/slf_notes.pdf.
This book will teach you about the foundations of Separation Logic, a practical approach to the modular verification of imperative programs. In particular, it presents the building blocks for constructing a program verification tool. It does not, however, focus on reasoning about data structures and algorithms using Separation Logic. This aspect is covered to some extent by Volume 5 of Software Foundations, which presents Verifiable C, a program logic and proof system for C. For OCaml programs, this aspect will be covered in a yet-to-be-written volume presenting CFML, a tool that builds upon all the techniques presented in this volume.
You are only assumed to understand the material in Software Foundations Volume 1 (Logical Foundations), and the two chapters on Hoare Logic (Hoare and Hoare2) from Software Foundations Volume 2 (PL Foundations). Volume 5 is not a prerequisite. The exposition here is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers.

Start Learning Find study partner
Books
University of Pennsylvania
Free
No Certificate

Software Foundation Volume 6: Separation Logic Foundations

via University of Pennsylvania
Start Learning Find study partner
Affiliate notice

  • Type
    Books
  • Provider
    University of Pennsylvania
  • Pricing
    Free
  • Certificate
    No Certificate

This electronic book is Volume 6 of the Software Foundations series, which presents the mathematical underpinnings of reliable software.

*COMPANION COURSE NOTES*: A large part of this course is also written up in traditional LaTeX-style presentation. It's available from http://www.chargueraud.org/teach/verif/slf_notes.pdf.
This book will teach you about the foundations of Separation Logic, a practical approach to the modular verification of imperative programs. In particular, it presents the building blocks for constructing a program verification tool. It does not, however, focus on reasoning about data structures and algorithms using Separation Logic. This aspect is covered to some extent by Volume 5 of Software Foundations, which presents Verifiable C, a program logic and proof system for C. For OCaml programs, this aspect will be covered in a yet-to-be-written volume presenting CFML, a tool that builds upon all the techniques presented in this volume.
You are only assumed to understand the material in Software Foundations Volume 1 (Logical Foundations), and the two chapters on Hoare Logic (Hoare and Hoare2) from Software Foundations Volume 2 (PL Foundations). Volume 5 is not a prerequisite. The exposition here is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers.

Quick Links

Browse by subject

Browse by provider

Browse by university

Browse by publisher

Browse by institution

Roadmaps

Posts