The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hi Coq-Club,

We are happy to announce the publication (on September 3, 2019) of an extensive survey of the scientific literature on proof engineering for software systems using proof assistants:

Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. QED at Large: A Survey of Engineering of Formally Verified Software. Foundations and Trends in Programming Languages (FTPL), Vol. 5: No. 2-3, pp 102-281, September 2019.

The article is available for free download at the URL above until around September 10, 2019.

---

Most of the authors are Coq users, and we believe the survey can be useful to the Coq community, both as a distillation of existing knowledge and for its comparisons with other proof assistants.

If you find any errors not already documented in our errata, please report them as a GitHub issue, submit a pull request for the errata source file, or contact us directly. Omissions are also welcome, as are questions about confusing text.

The small verified regular _expression_ matcher Coq project used as a motivating example in chapter 2 of the paper is available on Github.

And of course, thank you to everyone who helped make this possible.

Talia, Karl, Ilya, Milos, and Zach