This is the entry point to a series of electronic textbooks on various aspects of Software Foundations, the mathematical underpinnings of reliable software. Topics in the series include basic...

This electronic book is a survey of basic concepts in the mathematical study of programs and programming languages. Topics include advanced use of the Coq proof assistant, operational semantics,...

In this volume you will learn how to specify and verify (prove the correctness of) sorting algorithms, binary search trees, balanced binary search trees, and priority queues. Before using this book,...

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.QuickChick: Property-Based Testing in Coq introduces tools and techniques for combining...

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

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