C-rusted: The Advantages of Rust, in C, without the Disadvantages

• URL: http://arxiv.org/abs/2302.05331v3
• Date: Sat, 26 Aug 2023 14:41:10 GMT
• Title: C-rusted: The Advantages of Rust, in C, without the Disadvantages
• Authors: Roberto Bagnara, Abramo Bagnara, Federico Serafini
• Abstract summary: 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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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; dynamic properties of objects and the way they evolve during program execution; nominal typing and subtyping. The (partially) annotated C programs can be translated with unmodified versions of any compilation toolchain capable of processing ISO C code. The annotated C program parts can be validated by static analysis: if the static analyzer flags no error, then the annotations are provably coherent among themselves and with respect to annotated C code, in which case said annotated parts are provably exempt from a large class of logic, security, and run-time errors.

Related papers

• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages. This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• 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)
• Galapagos: Automated N-Version Programming with LLMs [10.573037638807024]
  We propose the automated generation of program variants using large language models. We design, develop and evaluate Gal'apagos: a tool for generating program variants. We evaluate Gal'apagos by creating N-Version components of real-world C code.
  arXiv  Detail & Related papers  (2024-08-18T16:44:01Z)
• C-LLM: Learn to Check Chinese Spelling Errors Character by Character [61.53865964535705]
  We propose C-LLM, a Large Language Model-based Chinese Spell Checking method that learns to check errors Character by Character. C-LLM achieves an average improvement of 10% over existing methods.
  arXiv  Detail & Related papers  (2024-06-24T11:16: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)
• C Analyzer : A Static Program Analysis Tool for C Programs [0.0]
  C Analyzer is a tool developed for static analysis of C programs. This project work tries to leverage Abstract Interpretation techniques for static analysis of C programs.
  arXiv  Detail & Related papers  (2024-01-28T11:43:16Z)
• LILO: Learning Interpretable Libraries by Compressing and Documenting Code [71.55208585024198]
  We introduce LILO, a neurosymbolic framework that iteratively synthesizes, compresses, and documents code. LILO combines LLM-guided program synthesis with recent algorithmic advances in automated from Stitch. We find that AutoDoc boosts performance by helping LILO's synthesizer to interpret and deploy learned abstractions.
  arXiv  Detail & Related papers  (2023-10-30T17:55:02Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42:18Z)
• CRIL: A Concurrent Reversible Intermediate Language [0.0]
  We present a reversible intermediate language with composing for translating a high-level concurrent programming language to another lower-level concurrent programming language, keeping reversibility. We propose CRIL as an extension of RIL used by Mogensen for a functional reversible language, incorporating a multi-thread process invocation and the synchronization primitives based on the P-V operations.
  arXiv  Detail & Related papers  (2023-09-13T20:52:54Z)
• Dcc --help: Generating Context-Aware Compiler Error Explanations with Large Language Models [53.04357141450459]
  dcc --help was deployed to our CS1 and CS2 courses, with 2,565 students using the tool over 64,000 times in ten weeks. We found that the LLM-generated explanations were conceptually accurate in 90% of compile-time and 75% of run-time cases, but often disregarded the instruction not to provide solutions in code.
  arXiv  Detail & Related papers  (2023-08-23T02:36:19Z)
• A Static Evaluation of Code Completion by Large Language Models [65.18008807383816]
  Execution-based benchmarks have been proposed to evaluate functional correctness of model-generated code on simple programming problems. static analysis tools such as linters, which can detect errors without running the program, haven't been well explored for evaluating code generation models. We propose a static evaluation framework to quantify static errors in Python code completions, by leveraging Abstract Syntax Trees.
  arXiv  Detail & Related papers  (2023-06-05T19:23:34Z)

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.