Description
Verifiable C is based on a 21st-century version of Hoare logic called higher-order impredicative concurrent separation logic. Back in the 20th century, computer scientists discovered that Hoare Logic was not very good at verifying programs with pointer data structures; so separation logic was developed. Hoare Logic was clumsy at verifying concurrent programs, so concurrent separation logic was developed. Hoare Logic could not handle higher-order object-oriented programming patterns or function-closures, so higher-order impredicative program logics were developed.
This electronic book is Volume 5 of the Software Foundations series, which presents the mathematical underpinnings of reliable software. The principal novelty of Software Foundations is that it is one hundred percent formalized and machine-checked: the entire text is literally a script for Coq. It is intended to be read alongside an interactive session with Coq. All the details in the text are fully formalized in Coq, and the exercises are designed to be worked using Coq.Before studying this volume, you should be a competent user of Coq:- Study Software Foundations Volume 1 (Logical Foundations), and do the exercises!
- Study the Hoare and Hoare2 chapters of Software Foundations Volume 2 (Programming Language Foundations), and do the exercises!
- Study the Sort, SearchTree, and ADT chapters of Software Foundations Volume 3 (Verified Functional Algorithms), and do the exercises!
Books 
University of Pennsylvania
Free 
No Certificate 
Software Foundation Volume 5: Verifiable C
-
TypeBooks
-
ProviderUniversity of Pennsylvania
-
PricingFree
-
CertificateNo Certificate
Verifiable C is based on a 21st-century version of Hoare logic called higher-order impredicative concurrent separation logic. Back in the 20th century, computer scientists discovered that Hoare Logic was not very good at verifying programs with pointer data structures; so separation logic was developed. Hoare Logic was clumsy at verifying concurrent programs, so concurrent separation logic was developed. Hoare Logic could not handle higher-order object-oriented programming patterns or function-closures, so higher-order impredicative program logics were developed.
This electronic book is Volume 5 of the Software Foundations series, which presents the mathematical underpinnings of reliable software. The principal novelty of Software Foundations is that it is one hundred percent formalized and machine-checked: the entire text is literally a script for Coq. It is intended to be read alongside an interactive session with Coq. All the details in the text are fully formalized in Coq, and the exercises are designed to be worked using Coq.Before studying this volume, you should be a competent user of Coq:- Study Software Foundations Volume 1 (Logical Foundations), and do the exercises!
- Study the Hoare and Hoare2 chapters of Software Foundations Volume 2 (Programming Language Foundations), and do the exercises!
- Study the Sort, SearchTree, and ADT chapters of Software Foundations Volume 3 (Verified Functional Algorithms), and do the exercises!
