@conference{262, author = {T. Runge and I. Schaefer and L.G.W.A. Cleophas and T. Thum and D.G Kourie and Bruce Watson}, 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.}, year = {2019}, journal = { European Joint Conferences on Theory and Practice of Software (ETAPS)}, chapter = {25 - 42}, month = {06/04 - 11/04}, publisher = {Springer}, address = {Switzerland}, isbn = {78-3-030-16721-9}, url = {https://link.springer.com/content/pdf/10.1007/978-3-030-16722-6.pdf}, doi = {https://doi.org/10.1007/978-3-030-16722-6 _ 2}, }