Tool support for correctness-by-construction

Tobias Runge, Ina Schaefer, Loek Cleophas, Thomas Thüm, Derrick Kourie, Bruce W. Watson

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

14 Downloads (Pure)

Abstract

Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC is supposed to lead to code with a low defect rate, it is not prevalent, especially because appropriate tool support is missing. To promote CbC, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation shows that our tool reduces the verification time in comparison to post-hoc verification.

Original languageEnglish
Title of host publicationFundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
EditorsReiner Hähnle, Wil van der Aalst
PublisherSpringer
Pages25-42
Number of pages18
ISBN (Print)9783030167219
DOIs
Publication statusPublished - 1 Jan 2019
Event22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Czech Republic
Duration: 6 Apr 201911 Apr 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11424 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019
CountryCzech Republic
CityPrague
Period6/04/1911/04/19

Fingerprint

Tool Support
Correctness
Specifications
Specification
Refinement
Refining
Open Source
Defects
Evaluation
Theorem

Cite this

Runge, T., Schaefer, I., Cleophas, L., Thüm, T., Kourie, D., & Watson, B. W. (2019). Tool support for correctness-by-construction. In R. Hähnle, & W. van der Aalst (Eds.), Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (pp. 25-42). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11424 LNCS). Springer. https://doi.org/10.1007/978-3-030-16722-6_2
Runge, Tobias ; Schaefer, Ina ; Cleophas, Loek ; Thüm, Thomas ; Kourie, Derrick ; Watson, Bruce W. / Tool support for correctness-by-construction. Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. editor / Reiner Hähnle ; Wil van der Aalst. Springer, 2019. pp. 25-42 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{0e6db16b44c94a84a74afdb7ee00ce3b,
title = "Tool support for correctness-by-construction",
abstract = "Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC is supposed to lead to code with a low defect rate, it is not prevalent, especially because appropriate tool support is missing. To promote CbC, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation shows that our tool reduces the verification time in comparison to post-hoc verification.",
author = "Tobias Runge and Ina Schaefer and Loek Cleophas and Thomas Th{\"u}m and Derrick Kourie and Watson, {Bruce W.}",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-16722-6_2",
language = "English",
isbn = "9783030167219",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "25--42",
editor = "Reiner H{\"a}hnle and {van der Aalst}, Wil",
booktitle = "Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings",
address = "Germany",

}

Runge, T, Schaefer, I, Cleophas, L, Thüm, T, Kourie, D & Watson, BW 2019, Tool support for correctness-by-construction. in R Hähnle & W van der Aalst (eds), Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11424 LNCS, Springer, pp. 25-42, 22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, 6/04/19. https://doi.org/10.1007/978-3-030-16722-6_2

Tool support for correctness-by-construction. / Runge, Tobias; Schaefer, Ina; Cleophas, Loek; Thüm, Thomas; Kourie, Derrick; Watson, Bruce W.

Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. ed. / Reiner Hähnle; Wil van der Aalst. Springer, 2019. p. 25-42 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11424 LNCS).

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

TY - GEN

T1 - Tool support for correctness-by-construction

AU - Runge, Tobias

AU - Schaefer, Ina

AU - Cleophas, Loek

AU - Thüm, Thomas

AU - Kourie, Derrick

AU - Watson, Bruce W.

PY - 2019/1/1

Y1 - 2019/1/1

N2 - Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC is supposed to lead to code with a low defect rate, it is not prevalent, especially because appropriate tool support is missing. To promote CbC, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation shows that our tool reduces the verification time in comparison to post-hoc verification.

AB - Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC is supposed to lead to code with a low defect rate, it is not prevalent, especially because appropriate tool support is missing. To promote CbC, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers in refining a program by a sequence of refinement steps and in verifying the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation shows that our tool reduces the verification time in comparison to post-hoc verification.

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

U2 - 10.1007/978-3-030-16722-6_2

DO - 10.1007/978-3-030-16722-6_2

M3 - Conference contribution

AN - SCOPUS:85064893948

SN - 9783030167219

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 25

EP - 42

BT - Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings

A2 - Hähnle, Reiner

A2 - van der Aalst, Wil

PB - Springer

ER -

Runge T, Schaefer I, Cleophas L, Thüm T, Kourie D, Watson BW. Tool support for correctness-by-construction. In Hähnle R, van der Aalst W, editors, Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Springer. 2019. p. 25-42. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-16722-6_2