Flexible Correct-by-Construction Programming

• URL: http://arxiv.org/abs/2211.15261v4
• Date: Tue, 6 Jun 2023 14:35:21 GMT
• Title: Flexible Correct-by-Construction Programming
• Authors: Tobias Runge, Tabea Bordis, Alex Potanin, Thomas Th\"um, Ina Schaefer
• Abstract summary: We compare Correctness-by-Construction (CbC) with CbC-Block and TraitCbC. CbC allows to develop software in a structured and incremental way to ensure correctness. We provide for both approaches a programming guideline, which similar to CbC, leads to well-structured programs.
• Score: 2.8798933523190327
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Correctness-by-Construction (CbC) is an incremental program construction process to construct functionally correct programs. The programs are constructed stepwise along with a specification that is inherently guaranteed to be satisfied. CbC is complex to use without specialized tool support, since it needs a set of predefined refinement rules of fixed granularity which are additional rules on top of the programming language. Each refinement rule introduces a specific programming statement and developers cannot depart from these rules to construct programs. CbC allows to develop software in a structured and incremental way to ensure correctness, but the limited flexibility is a disadvantage of CbC. In this work, we compare classic CbC with CbC-Block and TraitCbC. Both approaches CbC-Block and TraitCbC, are related to CbC, but they have new language constructs that enable a more flexible software construction approach. We provide for both approaches a programming guideline, which similar to CbC, leads to well-structured programs. CbC-Block extends CbC by adding a refinement rule to insert any block of statements. Therefore, we introduce CbC-Block as an extension of CbC. TraitCbC implements correctness-by-construction on the basis of traits with specified methods. We formally introduce TraitCbC and prove soundness of the construction strategy. All three development approaches are qualitatively compared regarding their programming constructs, tool support, and usability to assess which is best suited for certain tasks and developers.

Related papers

• A Core Calculus for Type-safe Product Lines of C Programs [2.1757527612572316]
  Lightweight C (LC) is a calculus that formalizes a proper subset of the calculus C without preprocessor directives.<n> Colored LC (CLC) is endowed with C preprocessor directives.<n>We believe that the simple formalization provided by CLC could be useful also for teaching purposes.
  arXiv  Detail & Related papers  (2026-03-04T12:51:23Z)
• Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning [65.20602712957725]
  Caco is a novel framework that automates the synthesis of high-quality, verifiable, and diverse instruction-CoT reasoning data.<n>Our work establishes a paradigm for building self-sustaining, trustworthy reasoning systems without human intervention.
  arXiv  Detail & Related papers  (2025-10-05T07:59:24Z)
• Continual Learning on CLIP via Incremental Prompt Tuning with Intrinsic Textual Anchors [50.7383184560431]
  Continual learning (CL) enables deep networks to acquire new knowledge while avoiding catastrophic forgetting.<n>We propose a concise CL approach for CLIP based on incremental prompt tuning.<n>We show that our bidirectional supervision strategy enables more effective learning of new knowledge while reducing forgetting.
  arXiv  Detail & Related papers  (2025-05-27T03:51:37Z)
• C*: Unifying Programming and Verification in C [15.531046191957529]
  C* is a proof-integrated language design for C programming. It enables real-time verification by allowing programmers to embed proof-code blocks alongside implementation code. C* unifies implementation and proof code development by using C as the common language.
  arXiv  Detail & Related papers  (2025-04-03T03:22:22Z)
• Modified Condition/Decision Coverage in the GNU Compiler Collection [0.0]
  We describe the implementation of the masking Modified Condition/Decision Coverage (MC/DC) support in GCC 14. By analyzing the Binary Decision Diagrams we can observe the key property of MC/DC, the power to independently affect the outcome, and map to the edges of the Control Flow Graph.
  arXiv  Detail & Related papers  (2025-01-03T22:59:38Z)
• CGP++ : A Modern C++ Implementation of Cartesian Genetic Programming [0.0]
  The reference implementation of Cartesian Genetic Programming (CGP) was written in the C programming language. We propose the first modern C++ implementation of CGP that pursues object-oriented design and generic programming paradigm.
  arXiv  Detail & Related papers  (2024-06-13T12:22:08Z)
• The Road to Near-Capacity CV-QKD Reconciliation: An FEC-Agnostic Design [53.67135680812675]
  A new codeword-based QKD reconciliation scheme is proposed. Both the authenticated classical channel (ClC) and the quantum channel (QuC) are protected by separate forward error correction (FEC) coding schemes. The proposed system makes QKD reconciliation compatible with a wide range of FEC schemes.
  arXiv  Detail & Related papers  (2024-03-24T14:47:08Z)
• Strong Priority and Determinacy in Timed CCS [0.0]
  Building on the standard theory of process algebra with priorities, we identify a new scheduling mechanism, called "constructive reduction" We prove for a large class of "coherent" processes a confluence property for constructive reductions.
  arXiv  Detail & Related papers  (2024-03-07T16:02:31Z)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  Undefined behavior in C often causes devastating security vulnerabilities. We introduce SECOMP, a compiler for compartmentalized C code with machine-checked proofs. This is the first time such a strong criterion is proven for a mainstream programming language.
  arXiv  Detail & Related papers  (2024-01-29T16:32:36Z)
• Contextualization Distillation from Large Language Model for Knowledge Graph Completion [51.126166442122546]
  We introduce the Contextualization Distillation strategy, a plug-in-and-play approach compatible with both discriminative and generative KGC frameworks. Our method begins by instructing large language models to transform compact, structural triplets into context-rich segments. Comprehensive evaluations across diverse datasets and KGC techniques highlight the efficacy and adaptability of our approach.
  arXiv  Detail & Related papers  (2024-01-28T08:56:49Z)
• Structured Code Representations Enable Data-Efficient Adaptation of Code Language Models [45.588949280419584]
  We explore data-efficient adaptation of pre-trained code models by further pre-training and fine-tuning them with program structures. Although the models that we adapt have been pre-trained only on the surface form of programs, we find that a small amount of continual pre-training and fine-tuning on CSTs without changing the model architecture yields improvements over the baseline approach across various code tasks.
  arXiv  Detail & Related papers  (2024-01-19T14:27:44Z)
• CSL: Class-Agnostic Structure-Constrained Learning for Segmentation Including the Unseen [62.72636247006293]
  Class-Agnostic Structure-Constrained Learning is a plug-in framework that can integrate with existing methods. We propose soft assignment and mask split methodologies that enhance OOD object segmentation. Empirical evaluations demonstrate CSL's prowess in boosting the performance of existing algorithms spanning OOD segmentation, ZS3, and DA segmentation.
  arXiv  Detail & Related papers  (2023-12-09T11:06:18Z)
• Exploring Continual Learning for Code Generation Models [80.78036093054855]
  Continual Learning (CL) is an important aspect that remains underexplored in the code domain. We introduce a benchmark called CodeTask-CL that covers a wide range of tasks, including code generation, translation, summarization, and refinement. We find that effective methods like Prompt Pooling (PP) suffer from catastrophic forgetting due to the unstable training of the prompt selection mechanism.
  arXiv  Detail & Related papers  (2023-07-05T16:58:39Z)
• C-rusted: The Advantages of Rust, in C, without the Disadvantages [0.0]
  C-rusted is an innovative technology whereby C programs can be (partly) annotated so as to express: ownership, exclusivity and shareability of language, system and user-defined resources. The (partially) annotated C programs can be translated with unmodified versions of any compilation toolchain capable of processing ISO C code.
  arXiv  Detail & Related papers  (2023-02-10T15:48:09Z)
• Bayes risk CTC: Controllable CTC alignment in Sequence-to-Sequence tasks [63.189632935619535]
  Bayes risk CTC (BRCTC) is proposed to enforce the desired characteristics of the predicted alignment. By using BRCTC with another preference for early emissions, we obtain an improved performance-latency trade-off for online models.
  arXiv  Detail & Related papers  (2022-10-14T03:55:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.