Property-Based Testing: Climbing the Stairway to Verification
Research PaperIn Person
Property-based testing (PBT) is a powerful tool that is widely available
in modern programming languages. It has been used to reduce formal software verification effort.
We demonstrate how PBT can be used in conjunction with formal verification to incrementally gain greater assurance in code correctness by integrating PBT into the verification framework of Cogent—a programming language equipped with a certifying compiler for developing
high-assurance systems components.
Specifically, for PBT and formal verification to work in tandem,
we structure the tests to mirror the refinement proof that we used in Cogent's verification framework:
The expected behaviour of the system under test is captured by a functional correctness specification,
which mimics the formal specification of the system, and we test the refinement relation between the
implementation and the specification. We exhibit the additional benefits that this
mutualism brings to developers and demonstrate the techniques we used in this style
of PBT, by studying two concrete examples.
Wed 7 DecDisplayed time zone: Auckland, Wellington change
15:30 - 16:57
|Lang-n-Prove: A DSL for Language ProofsVirtualResearch Paper
Matteo Cimini University of Massachusetts LowellDOI
|Property-Based Testing: Climbing the Stairway to VerificationResearch PaperIn Person
Zilin Chen UNSW, Christine Rizkallah University of Melbourne, Liam O'Connor University of Edinburgh, Partha Susarla Independent, Gerwin Klein Proofcraft; UNSW, Gernot Heiser UNSW, Gabriele Keller Utrecht UniversityDOI
|jGuard: Programming Misuse-Resilient APIsResearch PaperIn Person
Simon Binder TU Darmstadt, Krishna Narasimhan TU Darmstadt, Svenja Kernig TU Darmstadt, Mira Mezini TU DarmstadtDOI
|signatr: A Data-Driven Fuzzing Tool for RTool PaperIn Person
Alexi Turcotte Northeastern University, Pierre Donat-Bouillud Czech Technical University in Prague, Filip Křikava Czech Technical University in Prague, Jan Vitek Northeastern UniversityDOI