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
- 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) - Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods [1.2152813244704233]
We investigate how combinations of Large Language Models and symbolic analyses can be used to synthesise specifications of C programs.
The method infers rather the programs intent than its behaviour, by generating specifications for buggy programs and observing robustness of the result against bugs.
arXiv Detail & Related papers (2024-06-21T17:39:57Z) - Enabling Memory Safety of C Programs using LLMs [5.297072277460838]
Memory safety violations in low-level code, written in languages like C, continue to remain one of the major sources of software vulnerabilities.
One method of removing such violations by construction is to port C code to a safe C dialect.
Such dialects rely on programmer-supplied annotations to guarantee safety with minimal runtime overhead.
This porting is a manual process that imposes significant burden on the programmer and hence, there has been limited adoption of this technique.
arXiv Detail & Related papers (2024-04-01T13:05:54Z) - 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) - Extending C++ for Heterogeneous Quantum-Classical Computing [56.782064931823015]
qcor is a language extension to C++ and compiler implementation that enables heterogeneous quantum-classical programming, compilation, and execution in a single-source context.
Our work provides a first-of-its-kind C++ compiler enabling high-level quantum kernel (function) expression in a quantum-language manner.
arXiv Detail & Related papers (2020-10-08T12:49:07Z)
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.