Tool support for correctness-by-construction

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

1 Citaat (Scopus)
25 Downloads (Pure)

Samenvatting

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.

Originele taal-2Engels
TitelFundamental 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
RedacteurenReiner Hähnle, Wil van der Aalst
UitgeverijSpringer
Pagina's25-42
Aantal pagina's18
ISBN van geprinte versie9783030167219
DOI's
StatusGepubliceerd - 1 jan 2019
Evenement22nd 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, Tsjechië
Duur: 6 apr 201911 apr 2019

Publicatie series

NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11424 LNCS
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349

Congres

Congres22nd 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
LandTsjechië
StadPrague
Periode6/04/1911/04/19

Vingerafdruk Duik in de onderzoeksthema's van 'Tool support for correctness-by-construction'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    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 (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 (blz. 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