Trustworthy Systems

The Cogent case for property-based testing

Authors

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

DATA61

UNSW Sydney

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.

BibTeX Entry

  @inproceedings{Chen_OKKH_17,
    address          = {Shanghai, China},
    author           = {Chen, Zilin and O'Connor, Liam and Keller, Gabriele and Klein, Gerwin and Heiser, Gernot},
    booktitle        = {Workshop on Programming Languages and Operating Systems (PLOS)},
    date             = {2017-10-28},
    doi              = {https://doi.org/10.1145/3144555.3144556},
    isbn             = {9781450351539},
    month            = oct,
    pages            = {1-7},
    paperurl         = {https://trustworthy.systems/publications/full_text/Chen_OKKH_17.pdf},
    publisher        = {ACM},
    title            = {The {Cogent} Case for Property-Based Testing},
    year             = {2017}
  }

Download