Correctness-by-Construction (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 Correctness-by-Construction 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 Control-by-Construction

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 Control-by-Construction (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 semi-lattice (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.

Correctness-by-Construction 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 Correctness-by-Construction. VarCorC uses FeatureIDE and variational CbC to support the development of correctness-by-construction software product lines.

Publications

• M. Kodetzki, T. Bordis, T. Runge, and I. Schaefer. Partial Proofs to Optimize Deductive Verification of Feature-Oriented Software Product Lines. In 18th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS'24), 2024.
• T. Runge, T. Bordis, A. Potanin, T. Thüm, and I. Schaefer. Flexible Correct-by-Construction Programming. In Logical Methods in Computer Science, Volume 19, 2023.
• T. Runge. Correctness-by-Construction 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 Correct-by-Construction Programming. In CoRR 2022.
• T. Bordis, T. Runge, D. Schultz, and I.Schaefer. Family-Based and Product-Based Development of Correct-by-Construction Software Product Lines. In Journal of Computer Languages (COLA), 2022.
• T. Bordis, L. Cleophas, A. Kittelmann, T. Runge, I. Schaefer, and B. W. Watson. Re-CorC-ing KeY: Correct-by-Construction 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: Correctness-by-Construction for Free. In FORTE 2022.
• A. Kittelmann, T. Runge, T. Bordis, and I. Schaefer. Runtime Verification of Correct-by-Construction Driving Maneuvers. ISoLA 2022.
• T. Bordis, M. Kodetzki, T. Runge, and I. Schaefer. VarCorC: Developing Object-Oriented Software Product Lines Using Correctness-by-Construction. In SEFM Workshops, 2022.
• T. Runge, A. Kittelmann, M. Servetto, A. Potanin, and I. Schaefer. Information Flow Control-by-Construction for an Object-Oriented Language. SEFM 2022.
• I. Schaefer, T. Runge, L. Cleophas, and B. W. Watson. Tutorial: The Correctness-by-Construction Approach to Programming Using CorC. SecDev, 2021.
• T. Runge, T. Bordis, T. Thüm, and I. Schaefer. Teaching Correctness-by-Construction and Post-hoc Verification - The Online Experience. FMTea, 2021.
• T. Bordis, T. Runge, and I. Schaefer. Correctness-by-Construction for Feature-Oriented Software Product Lines. In GPCE, 2020.
• T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. Lattice-Based Information Flow Control-by-Construction for Security-by-Design. In FormaliSE, 2020.
• A. Knüppel, T. Runge, and I. Schaefer. Scaling Correctness-by-Construction. ISoLA, 2020.
• T. Bordis, T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. Variational Correctness-by-Construction. In 14th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS'20), 2020.
• T. Runge, T. Thüm, L. Cleophas, I. Schaefer, and B. W. Watson: Comparing Correctness-by-Construction with Post-Hoc 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 Correctness-by-Construction, 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 Cyber-Resilience in Critical Software-Intensive Systems (HILT'18), 2018.
• I. Schaefer, T. Runge, A. Knüppel, L. Cleophas, D. G. Kourie, and B. W. Watson: Towards Confidentiality-by-Construction. In International Symposium on Leveraging Applications of Formal Methods, Springer, 2018.