CorrectnessbyConstruction (CbC)
 Contact:
Tabea Bordis, Maximilian Kodetzki, Rasmus Ronneberg, Ina Schaefer
 Startdate:
December 2017
 Enddate:

CorrectnessbyConstruction (CbC) is an approach to incrementally create correct programs. CbC starts with an abstract Hoare triple {P} S {Q} consisting of a precondition P, an abstract statement S, and a postcondition Q. Hoare triples represent total correctness assertions that valuate only to true if, beginning from the precondition, the postcondition is met after executing the eventually defined concrete program. With CbC, the Hoare triple is successively refined using a set of refinement rules to a concrete implementation, which satisfies the specification. The correctness is guaranteed because every refinement rule is proven sound and preserves the correctness of the program. CbC is implemted in the tool CorC. CorC is a graphical and textual IDE to construct algorithms following the CorrectnessbyConstruction approach. It supports CbC developers to refine a program by a sequence of refinement steps and to verify the correctness of these refinement steps using a theorem prover.
Information Flow ControlbyConstruction
Besides of verifying the functional correctness, refinements rules can also be utilized to ensure security of programs. An information flow policy defines how information may flow in a program (e.g., a flow from public to secret data is allowed, but the other way is prohibited). The extension of CbC to ensure security is called Information Flow ControlbyConstruction (IFbC). Programs are constructed incrementally using refinement rules to follow an information flow policy. In every refinement step, security and functional correctness of the program is guaranteed, such that insecure programs are prohibited by construction. The information flow policy can be specified in any bounded upper semilattice (i.e., security levels are arranged in a partially ordered set representing the allowed direction of information flow). IFbC is implemented in an extension of CorC.
CorrectnessbyConstruction for Software Product Lines
Software product lines provide systematic reuse of software and other artifacts paired with variability mechanisms in the code to implement whole product families rather than single software products. The commonalities and differences of the single variants are communicated as features, whose relationships are often modelled in feature models. Guaranteeing the correctness of a product line is especially challenging because of the number of possible variants resulting from the number of feature configurations and the variable code structures. To create a correct product line using CbC, we therefore extended the original CbC approach with a new refinement rule for a variability mechanism in the statements of the Hoare triple and combined it with contract composition for variability in the pre and postcondition. We call this extension variational CorrectnessbyConstruction. VarCorC uses FeatureIDE and variational CbC to support the development of correctnessbyconstruction software product lines.
Publications
 M. Kodetzki, T. Bordis, T. Runge, and I. Schaefer. Partial Proofs to Optimize Deductive Verification of FeatureOriented Software Product Lines. In 18th International Working Conference on Variability Modelling of SoftwareIntensive Systems (VaMoS'24), 2024.
 T. Runge, T. Bordis, A. Potanin, T. Thüm, and I. Schaefer. Flexible CorrectbyConstruction Programming. In Logical Methods in Computer Science, Volume 19, 2023.
 T. Runge. CorrectnessbyConstruction for Correct and Secure Software Systems. Dissertation, 2023.
 T. Runge, M. Servetto, A. Potanin, and I. Schaefer. Immutability and Encapsulation for Sound OO Information Flow Control. In ACM Transactions on Programming Languages and Systems, Volume 45, 2023.
 T. Runge, A. Potanin, T. Thüm, and I. Schaefer. Traits for CorrectbyConstruction Programming. In CoRR 2022.
 T. Bordis, T. Runge, D. Schultz, and I.Schaefer. FamilyBased and ProductBased Development of CorrectbyConstruction Software Product Lines. In Journal of Computer Languages (COLA), 2022.
 T. Bordis, L. Cleophas, A. Kittelmann, T. Runge, I. Schaefer, and B. W. Watson. ReCorCing KeY: CorrectbyConstruction Software Development Based on KeY. In The Logic of Software. A Tasting Menu of Formal Methods, 2022.
 T. Runge, A. Potanin, T. Thüm, and I. Schaefer. Traits: CorrectnessbyConstruction for Free. In FORTE 2022.
 A. Kittelmann, T. Runge, T. Bordis, and I. Schaefer. Runtime Verification of CorrectbyConstruction Driving Maneuvers. ISoLA 2022.
 T. Bordis, M. Kodetzki, T. Runge, and I. Schaefer. VarCorC: Developing ObjectOriented Software Product Lines Using CorrectnessbyConstruction. In SEFM Workshops, 2022.
 T. Runge, A. Kittelmann, M. Servetto, A. Potanin, and I. Schaefer. Information Flow ControlbyConstruction for an ObjectOriented Language. SEFM 2022.
 I. Schaefer, T. Runge, L. Cleophas, and B. W. Watson. Tutorial: The CorrectnessbyConstruction Approach to Programming Using CorC. SecDev, 2021.
 T. Runge, T. Bordis, T. Thüm, and I. Schaefer. Teaching CorrectnessbyConstruction and Posthoc Verification  The Online Experience. FMTea, 2021.
 T. Bordis, T. Runge, and I. Schaefer. CorrectnessbyConstruction for FeatureOriented Software Product Lines. In GPCE, 2020.
 T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. LatticeBased Information Flow ControlbyConstruction for SecuritybyDesign. In FormaliSE, 2020.
 A. Knüppel, T. Runge, and I. Schaefer. Scaling CorrectnessbyConstruction. ISoLA, 2020.
 T. Bordis, T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. Variational CorrectnessbyConstruction. In 14th International Working Conference on Variability Modelling of SoftwareIntensive Systems (VaMoS'20), 2020.
 T. Runge, T. Thüm, L. Cleophas, I. Schaefer, and B. W. Watson: Comparing CorrectnessbyConstruction with PostHoc Verification  A Qualitative User Study. In REFINE, 2019.
 T. Runge, I. Schaefer, L. Cleophas, T. Thüm, D. G. Kourie, and B. W. Watson: Tool Support for CorrectnessbyConstruction, Proc. of the International Conference on Fundamental Approaches to Software Engineering (FASE), Springer, 2019.
 T. Runge, I. Schaefer, A. Knüppel, L. Cleophas, D. G. Kourie, and B. W. Watson: Tool support for Confidentiality by Construction. In HILT 2018 Workshop on Languages and Tools for Ensuring CyberResilience in Critical SoftwareIntensive Systems (HILT'18), 2018.
 I. Schaefer, T. Runge, A. Knüppel, L. Cleophas, D. G. Kourie, and B. W. Watson: Towards ConfidentialitybyConstruction. In International Symposium on Leveraging Applications of Formal Methods, Springer, 2018.