The COGENT Case for Property-Based Testing

Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein, Gernot Heiser

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Property-based testing can play an important role in reducing the cost of formal verification: It has been demonstrated to be effective at detecting bugs and finding inconsistencies in specifications, and thus can eliminate effort wasted on fruitless proof attempts. We argue that in addition, property-based testing enables an incremental approach to a fully verified system, by allowing replacement of automatically generated tests of properties stated in the specification by formal proofs. We demonstrate this approach on the verification of systems code, discuss the implications on systems design, and outline the integration of property-based testing into the Cogent framework.
Original languageEnglish
Title of host publicationProceedings of the 9th Workshop on Programming Languages and Operating Systems
Place of PublicationNew York, NY, USA
PublisherACM Association for Computing Machinery
Pages1–7
Number of pages7
ISBN (Print)9781450351539
DOIs
Publication statusPublished - 31 Oct 2017
Event9th Workshop on Programming Languages and Operating Systems - Shanghai, China
Duration: 28 Oct 201728 Oct 2017
https://ess.cs.tu-dortmund.de/workshops/plos/2017/home.php

Workshop

Workshop9th Workshop on Programming Languages and Operating Systems
Abbreviated titlePLOS 2017
Country/TerritoryChina
CityShanghai
Period28/10/1728/10/17
Internet address

Keywords / Materials (for Non-textual outputs)

  • Cogent
  • Formal methods
  • QuickCheck
  • Refinement
  • Systems software

Fingerprint

Dive into the research topics of 'The COGENT Case for Property-Based Testing'. Together they form a unique fingerprint.

Cite this