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

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

doi:10.1007/978-3-319-47166-2_52

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

6 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 language	English
Title of host publication	ISoLA 2016: Leveraging Applications of Formal Methods, Verification and Validation : Foundational Techniques
Subtitle of host publication	7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I
Editors	T. Margaria, B. Steffen
Place of Publication	Dordrecht
Publisher	Springer
Pages	730-748
ISBN (Electronic)	978-3-319-47166-2
ISBN (Print)	978-3-319-47165-5
DOIs	https://doi.org/10.1007/978-3-319-47166-2_52
Publication status	Published - 5 Oct 2016

Publication series

Name	LNCS
Volume	9952

Access to Document

10.1007/978-3-319-47166-2_52

http://link.springer.com/10.1007/978-3-319-47166-2_52

Fingerprint Dive into the research topics of 'Correctness-by-construction and post-hoc verification : a marriage of convenience?'. Together they form a unique 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). Springer. https://doi.org/10.1007/978-3-319-47166-2_52

Watson, B.W. ; Kourie, D.G. ; Schaefer, I. ; Cleophas, L.G.W.A. / Correctness-by-construction and post-hoc verification : a marriage of convenience?. 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. editor / T. Margaria ; B. Steffen. Dordrecht : Springer, 2016. pp. 730-748 (LNCS).

@inproceedings{c4069c3b5f044be3b7c63587bb9f705f,

title = "Correctness-by-construction and post-hoc verification : a marriage of convenience?",

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

author = "B.W. Watson and D.G. Kourie and I. Schaefer and L.G.W.A. Cleophas",

year = "2016",

month = oct,

day = "5",

doi = "10.1007/978-3-319-47166-2_52",

language = "English",

isbn = "978-3-319-47165-5",

series = "LNCS",

publisher = "Springer",

pages = "730--748",

editor = "T. Margaria and B. Steffen",

booktitle = "ISoLA 2016: Leveraging Applications of Formal Methods, Verification and Validation : Foundational Techniques",

address = "Germany",

}

Watson, BW, Kourie, DG, Schaefer, I & Cleophas, LGWA 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. LNCS, vol. 9952, Springer, Dordrecht, pp. 730-748. https://doi.org/10.1007/978-3-319-47166-2_52

Correctness-by-construction and post-hoc verification : a marriage of convenience? / Watson, B.W.; Kourie, D.G.; Schaefer, I.; Cleophas, L.G.W.A.

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. ed. / T. Margaria; B. Steffen. Dordrecht : Springer, 2016. p. 730-748 (LNCS; Vol. 9952).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review