Correctness-by-construction and post-hoc verification : a marriage of convenience?

B.W. Watson, D.G. Kourie, I. Schaefer, L.G.W.A. Cleophas

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)
3 Downloads (Pure)

Abstract

Correctness-by-construction (CbC), traditionally based on weakest precondition semantics, and post-hoc verification (PhV) aspire to ensure functional correctness. We argue for a lightweight approach to CbC where lack of formal rigour increases productivity. In order to mitigate the risk of accidentally introducing errors during program construction, we propose to complement lightweight CbC with PhV. We introduce lightweight CbC by example and discuss strength and weaknesses of CbC and PhV and their combination, both conceptually and using a case study.
Original languageEnglish
Title of host publicationISoLA 2016: Leveraging Applications of Formal Methods, Verification and Validation : Foundational Techniques
Subtitle of host publication7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I
EditorsT. Margaria, B. Steffen
Place of PublicationDordrecht
PublisherSpringer
Pages730-748
ISBN (Electronic)978-3-319-47166-2
ISBN (Print)978-3-319-47165-5
DOIs
Publication statusPublished - 5 Oct 2016

Publication series

NameLNCS
Volume9952

    Fingerprint

Cite this

Watson, B. W., Kourie, D. G., Schaefer, I., & Cleophas, L. G. W. A. (2016). Correctness-by-construction and post-hoc verification : a marriage of convenience? In T. Margaria, & B. Steffen (Eds.), ISoLA 2016: Leveraging Applications of Formal Methods, Verification and Validation : Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I (pp. 730-748). (LNCS; Vol. 9952). Dordrecht: Springer. https://doi.org/10.1007/978-3-319-47166-2_52