Kodetzki, MaximilianBordis, TabeaPotanin, AlexSchaefer, Ina2026-03-042026-03-049798400721519ORCID:/0000-0002-4242-2725/work/207109943https://hdl.handle.net/1885/733807102Correctness-by-Construction engineering (CbC) is a refinement-based approach to develop functionally correct programs based on a formal specification. By correctly applying refinement rules during development, CbC enables detection of bugs during program construction, unlike post-hoc verification, which proves correctness only after implementation. Support for CbC engineering for non-functional properties is summarized under the term X-by-Construction (XbC). However, current XbC approaches are limited to information flow properties, leaving other non-functional properties of software quality, such as performance or reliability, unsupported. To address this gap, we present our vision for generalizing XbC to integrate non-functional properties into by-Construction engineering. In this way, we leverage the development of high-quality software through a refinement-based approach for future software engineering. With that, it will become possible to develop software ensuring that it not only exhibits functional correctness, but also non-functional guarantees by construction. Further, we propose ideas for ensuring energy efficiency in by-Construction engineering. We assess what it needs to integrate non-functional properties into by-Construction engineering and discuss arising challenges.This work was partially supported by funding from the pilot program Core-Informatics of the Helmholtz Association (HGF).17enPublisher Copyright: © 2025 Owner/Author.Correctness-by-ConstructionEnergy EfficiencyFormal MethodsResource ConsumptionSoftware Quality2025-10-0910.1145/3759429.3762623105021397611