論文の概要: C-rusted: The Advantages of Rust, in C, without the Disadvantages
- arxiv url: http://arxiv.org/abs/2302.05331v3
- Date: Sat, 26 Aug 2023 14:41:10 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-24 13:13:46.966659
- Title: C-rusted: The Advantages of Rust, in C, without the Disadvantages
- Title(参考訳): c-rusted: 欠点のないcにおけるrustのメリット
- Authors: Roberto Bagnara, Abramo Bagnara, Federico Serafini
- Abstract要約: C-rustedは、言語、システム、およびユーザ定義リソースのオーナシップ、排他性、共有性を表現するために(部分的に)Cプログラムに注釈を付けることができる革新的な技術である。
注釈付きCプログラムは、ISO Cコードを処理することができるコンパイルツールチェーンの修正されていないバージョンで変換することができる。
- 参考スコア(独自算出の注目度): 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.
- Abstract(参考訳): c-rustedは、言語、システム、ユーザ定義リソースの所有権、排他性と共有性、オブジェクトの動的特性とプログラム実行中の進化方法、名目的型付けとサブタイプなどを表現するためにcプログラムを(部分的に)アノテートできる革新的な技術である。
注釈付きCプログラムは、ISO Cコードを処理することができるコンパイルツールチェーンの修正されていないバージョンで変換することができる。
静的アナライザがエラーを警告しない場合、アノテーションはそれ自身と注釈付きCコードの間で確実に一貫性があり、この場合、アノテーション付き部分は大規模な論理クラス、セキュリティ、実行時のエラーから確実に除外される。
関連論文リスト
- Enabling Memory Safety of C Programs using LLMs [5.297072277460838]
C言語で書かれた低レベルのコードのメモリ安全性違反は、ソフトウェア脆弱性の主要な原因のひとつであり続けています。
このような違反を建設によって除去する方法の1つは、安全なC方言にCコードを移植することである。
このような方言は、最小限のランタイムオーバーヘッドで安全性を保証するためにプログラマが提供するアノテーションに依存している。
この移植は、プログラマに多大な負担をかける手作業であり、そのため、このテクニックの採用は限られている。
論文 参考訳(メタデータ) (2024-04-01T13:05:54Z) - SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。
本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。
このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
論文 参考訳(メタデータ) (2024-01-29T16:32:36Z) - C Analyzer : A Static Program Analysis Tool for C Programs [0.0]
C Analyzerは、Cプログラムの静的解析のために開発されたツールである。
本研究は,Cプログラムの静的解析に抽象解釈技術を活用することを目的とする。
論文 参考訳(メタデータ) (2024-01-28T11:43:16Z) - LILO: Learning Interpretable Libraries by Compressing and Documenting Code [71.55208585024198]
LILOは、反復的に合成、圧縮、文書化を行う、ニューロシンボリックなフレームワークである。
LILOは、LLM誘導プログラム合成と、Stitchから自動化された最近のアルゴリズムの進歩を組み合わせたものである。
LILOのシンセサイザーが学習した抽象化を解釈し、デプロイするのを手助けすることで、AutoDocがパフォーマンスを向上させることが分かりました。
論文 参考訳(メタデータ) (2023-10-30T17:55:02Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳(メタデータ) (2023-09-25T15:42:18Z) - CRIL: A Concurrent Reversible Intermediate Language [0.0]
本稿では,高レベル並列言語を他の低レベル並列言語に翻訳するための構成の可逆中間言語を提案し,可逆性を維持する。
機能的可逆言語としてMogensen が用いた RIL の拡張として CRIL を提案し,P-V 演算に基づくマルチスレッドプロセス呼び出しと同期プリミティブを組み込んだ。
論文 参考訳(メタデータ) (2023-09-13T20:52:54Z) - Dcc --help: Generating Context-Aware Compiler Error Explanations with
Large Language Models [53.04357141450459]
dcc --helpはCS1とCS2のコースにデプロイされ、2565人の学生が10週間で64,000回以上このツールを使っている。
LLMが生成した説明は、コンパイル時間の90%と実行時の75%で概念的に正確であるが、コードに解決策を提供しない命令を無視することが多かった。
論文 参考訳(メタデータ) (2023-08-23T02:36:19Z) - A Static Evaluation of Code Completion by Large Language Models [65.18008807383816]
単純なプログラミング問題に対するモデル生成コードの機能的正当性を評価するために,実行ベースベンチマークが提案されている。
プログラムを実行せずにエラーを検出するlinterのような静的解析ツールは、コード生成モデルを評価するために十分に研究されていない。
抽象構文木を利用して,Pythonのコード補完における静的エラーを定量化する静的評価フレームワークを提案する。
論文 参考訳(メタデータ) (2023-06-05T19:23:34Z) - Synchromesh: Reliable code generation from pre-trained language models [38.15391794443022]
コード生成のための事前学習モデルの信頼性を大幅に向上するフレームワークであるSynchromeshを提案する。
まず、TST(Target similarity Tuning)を使用して、トレーニングバンクから、セマンティックなサンプル選択の新しい方法を使用して、数ショットのサンプルを検索する。
次に、Synchromeshはサンプルをトレーニング済みの言語モデルに供給し、対象言語の有効なプログラムセットに出力を制約する一般的なフレームワークであるConstrained Semantic Decoding (CSD)を使用してプログラムをサンプリングする。
論文 参考訳(メタデータ) (2022-01-26T22:57:44Z) - LM-Critic: Language Models for Unsupervised Grammatical Error Correction [128.9174409251852]
文を文法的に判断する LM-Critic の定義において,事前訓練された言語モデル (LM) の活用法を示す。
このLM-Critic と BIFI と、ラベルなし文の集合を併用して、現実的な非文法的/文法的ペアをブートストラップし、修正子を訓練する。
論文 参考訳(メタデータ) (2021-09-14T17:06:43Z) - Extending C++ for Heterogeneous Quantum-Classical Computing [56.782064931823015]
qcorはC++とコンパイラの実装の言語拡張で、異種量子古典プログラミング、コンパイル、単一ソースコンテキストでの実行を可能にする。
我々の研究は、量子言語で高レベルな量子カーネル(関数)を表現できる、第一種C++コンパイラを提供する。
論文 参考訳(メタデータ) (2020-10-08T12:49:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。