The COGENT case for property-based testing

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

doi:10.1145/3144555.3144556

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 proceeding › Conference contribution › Academic › peer-review

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 language	English
Title of host publication	Proceedings of the 9th Workshop on Programming Languages and Operating Systems, PLOS 2017
Publisher	Association for Computing Machinery
Pages	1-7
Number of pages	7
ISBN (Electronic)	9781450351539
DOIs	https://doi.org/10.1145/3144555.3144556
Publication status	Published - 28 Oct 2017
Externally published	Yes
Event	9th Workshop on Programming Languages and Operating Systems, PLOS 2017 - Shanghai, China Duration: 28 Oct 2017 → …

Conference

Conference	9th Workshop on Programming Languages and Operating Systems, PLOS 2017
Country/Territory	China
City	Shanghai
Period	28/10/17 → …

Keywords

COGENT
Formal methods
QuickCheck
Refinement
Systems software

Access to Document

10.1145/3144555.3144556

Cite this

@inproceedings{bf547d8b32f14403918b1ef8621d7f0c,

title = "The COGENT case for property-based testing",

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.",

keywords = "COGENT, Formal methods, QuickCheck, Refinement, Systems software",

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

year = "2017",

month = oct,

day = "28",

doi = "10.1145/3144555.3144556",

language = "English",

pages = "1--7",

booktitle = "Proceedings of the 9th Workshop on Programming Languages and Operating Systems, PLOS 2017",

publisher = "Association for Computing Machinery",

address = "United States",

note = "9th Workshop on Programming Languages and Operating Systems, PLOS 2017 ; Conference date: 28-10-2017",

}

Chen, Z, O'Connor, L, Keller, G, Klein, G & Heiser, G 2017, The COGENT case for property-based testing. in Proceedings of the 9th Workshop on Programming Languages and Operating Systems, PLOS 2017. Association for Computing Machinery, pp. 1-7, 9th Workshop on Programming Languages and Operating Systems, PLOS 2017, Shanghai, China, 28/10/17. https://doi.org/10.1145/3144555.3144556

TY - GEN

T1 - The COGENT case for property-based testing

AU - Chen, Zilin

AU - O'Connor, Liam

AU - Keller, Gabriele

AU - Klein, Gerwin

AU - Heiser, Gernot

PY - 2017/10/28

Y1 - 2017/10/28

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

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

KW - COGENT

KW - Formal methods

KW - QuickCheck

KW - Refinement

KW - Systems software

UR - http://www.scopus.com/inward/record.url?scp=85037103727&partnerID=8YFLogxK

U2 - 10.1145/3144555.3144556

DO - 10.1145/3144555.3144556

M3 - Conference contribution

AN - SCOPUS:85037103727

SP - 1

EP - 7

BT - Proceedings of the 9th Workshop on Programming Languages and Operating Systems, PLOS 2017

PB - Association for Computing Machinery

T2 - 9th Workshop on Programming Languages and Operating Systems, PLOS 2017

Y2 - 28 October 2017

ER -

The COGENT case for property-based testing

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this