Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeY

Tabea Bordis, Loek Cleophas, Alexander Kittelmann, Tobias Runge, Ina Schaefer, Bruce W. Watson

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

3 Citations (Scopus)

Abstract

Deductive program verification is a post-hoc quality assurance technique following the design-by-contract paradigm where correctness of the program is proven only after it was written. Contrary, correctness-by-construction (CbC) is an incremental program construction technique. Starting with the functional specification, the program’s correctness is guaranteed by application of a small set of refinement rules. Even though CbC is supposed to lead to code with a low defect rate and improve the traceability of errors, it is not widespread. One of the main reasons is insufficient tool support which we addressed with our tool CorC. CorC provides support for CbC-based program construction with the KeY program verifier as backend prover for checking correctness of refinement rule applications. However, CorC was limited to constructing single method bodies restricting its applicability. In this work, we introduce and discuss CorC 2.0, which extends CorC ’s programming model with objects as used in object-oriented programming. We integrate CorC into a development process that allows to use post-hoc verification and CbC interchangeably to construct correct programs, and scale the applicability of CbC on the architectural level in our tool extension ArchiCorC. We developed three object-oriented case studies and evaluated the verification effort and the usability of CorC in comparison to post-hoc verification.

Original languageEnglish
Title of host publicationThe Logic of Software. A Tasting Menu of Formal Methods
Subtitle of host publicationEssays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday
EditorsWolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Einar Broch Johnsen
PublisherSpringer
Pages80-104
Number of pages25
ISBN (Electronic)978-3-031-08166-8
ISBN (Print)978-3-031-08165-1
DOIs
Publication statusPublished - 2022

Publication series

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

Bibliographical note

Publisher Copyright:
© 2022, Springer Nature Switzerland AG.

Fingerprint

Dive into the research topics of 'Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeY'. Together they form a unique fingerprint.

Cite this