Leonidas Lampropoulos
2018-08-29 16:12:07 UTC
We are pleased to announce the release of a new fourth volume in the Software Foundations series, entitled QuickChick: Property-Based Testing in Coq.
https://softwarefoundations.cis.upenn.edu/qc-current/index.html
This new volume describes QuickChick, a property-based random testing tool for Coq, and introduces techniques for combining random testing with formal specification and proof in the Coq ecosystem. The combination enables Coq users to quickly debug theorems and definitions before embarking on manual proof efforts. Basic knowledge of Coq (e.g., from Logical Foundations, Volume 1 of Software Foundations) is assumed; property-based testing is introduced from scratch.
For a semester course based on Software Foundations, this volume can serve as a basis for a short series of 3 or 4 lectures, following Logical Foundations and before proceeding to either Programming Language Foundations (Volume 2) or Verified Functional Algorithms (Volume 3). This will allow students to leverage random testing when working on the exercises of the more advanced material.
We hope you enjoy this volume and look forward to any feedback you may have.
Leo and Benjamin
Leonidas Lampropoulos
***@seas.upenn.edu<mailto:***@seas.upenn.edu>
Benjamin C. Pierce
***@cis.upenn.edu<mailto:***@cis.upenn.edu>
[cid:a96b3d3d-dab3-4792-99c3-a5d58319ba64]
https://softwarefoundations.cis.upenn.edu/qc-current/index.html
This new volume describes QuickChick, a property-based random testing tool for Coq, and introduces techniques for combining random testing with formal specification and proof in the Coq ecosystem. The combination enables Coq users to quickly debug theorems and definitions before embarking on manual proof efforts. Basic knowledge of Coq (e.g., from Logical Foundations, Volume 1 of Software Foundations) is assumed; property-based testing is introduced from scratch.
For a semester course based on Software Foundations, this volume can serve as a basis for a short series of 3 or 4 lectures, following Logical Foundations and before proceeding to either Programming Language Foundations (Volume 2) or Verified Functional Algorithms (Volume 3). This will allow students to leverage random testing when working on the exercises of the more advanced material.
We hope you enjoy this volume and look forward to any feedback you may have.
Leo and Benjamin
Leonidas Lampropoulos
***@seas.upenn.edu<mailto:***@seas.upenn.edu>
Benjamin C. Pierce
***@cis.upenn.edu<mailto:***@cis.upenn.edu>
[cid:a96b3d3d-dab3-4792-99c3-a5d58319ba64]