# Preface

# Welcome

- Write your program in an expressive language with a good proof theory (the Gallina language embedded in Coq's logic).
- Prove it correct in Coq.
- Extract it to ML and compile it with an optimizing ML compiler.

*Verifiable C*, a program logic and proof system for C.

*Programming Language Foundations*volume of this series. (If you have not done so already, study the Hoare and Hoare2 chapters of that volume, and do the exercises.)

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

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

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

# Practicalities

## System Requirements

*IF YOU USE OPAM*, the following opam commands may be useful:

- opam repo add coq-released
- opam pin coq 8.12.0
- opam install coq-vst.2.6 (
*this will take 30 minutes or more*) - (to use coqide:) opam pin lablgtk3 3.0.beta5
- (to use coqide:) opam install coqide

*You do not need to install CompCert clightgen*to do the exercises in this volume. But if you wish to modify and reparse the .c files, or verify C programs of your own, install the CompCert verified optimizing C compiler. You can get CompCert from compcert.inria.fr, or (starting with Coq 8.12) in the standard "Coq Package" or by opam (the package is named coq-compcert).

## Downloading the Coq Files

## Installation

## Exercises

- One star: easy exercises that underscore points in the text
and that, for most readers, should take only a minute or two.
Get in the habit of working these as you reach them.
- Two stars: straightforward exercises (five or ten minutes).
- Three stars: exercises requiring a bit of thought (ten
minutes to half an hour).
- Four and five stars: more difficult exercises (half an hour and up).

*Please do not post solutions to the exercises in any public place*: Software Foundations is widely used both for self-study and for university courses. Having solutions easily available makes it much less useful for courses, which typically have graded homework assignments. The authors especially request that readers not post solutions to the exercises anyplace where they can be found by search engines.

## Recommended Citation Format

@book {Appel:SF5,

author = {Andrew W. Appel and Qinxiang Cao},

title = "Verifiable C",

series = "Software Foundations",

volume = "5",

year = "2020",

publisher = "Electronic textbook",

note = {Version 0.9.7, \URL{http://softwarefoundations.cis.upenn.edu} },

}

## For Instructors and Contributors

*Logical Foundations*for instructions.

# Thanks

*Software Foundations*series has been supported, in part, by the National Science Foundation under the NSF Expeditions grant 1521523,

*The Science of Deep Specification*.

# Check for the right version of VST

Require Import Coq.Strings.String.

Open Scope string.

Require Import VST.veric.version. (* If this line fails, it means

you don't have a VST installed. *)

Goal release = "2.6".

reflexivity || fail "The wrong version of VST is installed".

Abort.

(* 2020-09-18 15:39 *)

Open Scope string.

Require Import VST.veric.version. (* If this line fails, it means

you don't have a VST installed. *)

Goal release = "2.6".

reflexivity || fail "The wrong version of VST is installed".

Abort.

(* 2020-09-18 15:39 *)