Tool support for correctness-by-construction
| dc.contributor.author | Runge, Tobias | en_ZA |
| dc.contributor.author | Schaefer, Ina | en_ZA |
| dc.contributor.author | Cleophas, Loek | en_ZA |
| dc.contributor.author | Thum, Thomas | en_ZA |
| dc.contributor.author | Kourie, Derrick | en_ZA |
| dc.contributor.author | Watson, Bruce W. | en_ZA |
| dc.date.accessioned | 2021-12-01T14:24:36Z | |
| dc.date.available | 2021-12-01T14:24:36Z | |
| dc.date.issued | 2019 | |
| dc.description | CITATION: 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.description | The original publication is available at https://link.springer.com | |
| dc.description.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. | en_ZA |
| dc.description.uri | https://link.springer.com/chapter/10.1007/978-3-030-16722-6_2 | |
| dc.description.version | Publisher's version | |
| dc.format.extent | 18 pages | |
| dc.identifier.citation | 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.identifier.issn | 1611-3349 (online) | |
| dc.identifier.issn | 0302-9743 (print) | |
| dc.identifier.other | doi:10.1007/978-3-030-16722-6_2 | |
| dc.identifier.uri | http://hdl.handle.net/10019.1/123515 | |
| dc.language.iso | en_ZA | en_ZA |
| dc.publisher | Springer | |
| dc.rights.holder | Authors retain copyright | |
| dc.subject | Computer programs -- Correctness | en_ZA |
| dc.title | Tool support for correctness-by-construction | en_ZA |
| dc.type | Article | en_ZA |