Tool support for correctness-by-construction

Simple item page
dc.contributor.authorRunge, Tobiasen_ZA
dc.contributor.authorSchaefer, Inaen_ZA
dc.contributor.authorCleophas, Loeken_ZA
dc.contributor.authorThum, Thomasen_ZA
dc.contributor.authorKourie, Derricken_ZA
dc.contributor.authorWatson, Bruce W.en_ZA
dc.date.accessioned2021-12-01T14:24:36Z
dc.date.available2021-12-01T14:24:36Z
dc.date.issued2019
dc.descriptionCITATION: Runge, T., et al. 2019. Tool support for correctness-by-construction. Lecture Notes in Computer Science, 11424:25-42, doi:10.1007/978-3-030-16722-6_2.
dc.descriptionThe original publication is available at https://link.springer.com
dc.description.abstractCorrectness-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.en_ZA
dc.description.urihttps://link.springer.com/chapter/10.1007/978-3-030-16722-6_2
dc.description.versionPublisher's version
dc.format.extent18 pages
dc.identifier.citationRunge, T., et al. 2019. Tool support for correctness-by-construction. Lecture Notes in Computer Science, 11424:25-42, doi:10.1007/978-3-030-16722-6_2
dc.identifier.issn1611-3349 (online)
dc.identifier.issn0302-9743 (print)
dc.identifier.otherdoi:10.1007/978-3-030-16722-6_2
dc.identifier.urihttp://hdl.handle.net/10019.1/123515
dc.language.isoen_ZAen_ZA
dc.publisherSpringer
dc.rights.holderAuthors retain copyright
dc.subjectComputer programs -- Correctnessen_ZA
dc.titleTool support for correctness-by-constructionen_ZA
dc.typeArticleen_ZA
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
runge_tool_2019.pdf
Size:
1.27 MB
Format:
Adobe Portable Document Format
Description:
Download article
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed upon to submission
Description:
Download
Collections
Research Articles (Computer Science)