تقرير
The CREUSOT Environment for the Deductive Verification of Rust Programs
| العنوان: | The CREUSOT Environment for the Deductive Verification of Rust Programs |
|---|---|
| المؤلفون: | Denis, Xavier, Jourdan, Jacques-Henri, Marché, Claude |
| المساهمون: | Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Inria Saclay - Île de France |
| المصدر: | https://inria.hal.science/hal-03526634Test ; [Research Report] RR-9448, Inria Saclay - Île de France. 2021. |
| بيانات النشر: | HAL CCSD |
| سنة النشر: | 2021 |
| المجموعة: | Université de Rennes 1: Publications scientifiques (HAL) |
| مصطلحات موضوعية: | Rust programming language, Formal Specification, Deductive verification, Aliasing and Ownership, Prophecies, Traits, Langage de programmation Rust, Spécification formelle, Vérification Déductive, Alias, Ownership, Prophéties, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] |
| الوصف: | Rust is a fairly recent programming language for system programming, bringing static guarantees of memory safety through a strong ownership policy. This feature opens promising advances for deductive verification of Rust code, which aims at proving the conformity of some code with respect to a specification of its intended behavior. In this report we present Creusot, a tool for the formal specification and deductive verification of Rust programs. There are two main original features in the approach implemented in Creusot. First, Creusot’s specification language features a notion of prophecies, which is central for the specification of behavior of programs performing memory mutation. Prophecies also permit efficient automated reasoning for verifying about such programs.Rust provides advanced abstraction features based on a notion of traits, extensively used in the standard library and in user code. The support for traits is the second main feature of Creusot, because it is at the heart of its approach, in particular for providing complex abstraction of the functional behavior of programs. ; Rust est un langage de programmation relativement récent pour la programmation système, apportant des garanties statiques de sûreté des accès mémoire à travers une politique rigoureuse d’ownership. Cette approche ouvre une voie prometteuse pour la vérification déductive de code Rust, qui vise à prouver la conformité d’un code vis-à-vis d’une spécification de son comportement prévu. Dans ce rapport nous présentons CREUSOT, un outil pour la spécification formelle et la vérification déductive de programmes Rust.L’approche mise en œuvre dans CREUSOT s’appuie sur deux caractéristiques originales. Premièrement, le langage de spécification de CREUSOT fournit une notion de prophétie, qui est centrale pour la spécification du comportement des programmes effectuant des modifications en place de la mémoire. Les prophéties permettent aussi un raisonnement automatisé efficace pour vérifier ces programmes.Rust fournit des fonctionnalités ... |
| نوع الوثيقة: | report |
| اللغة: | English |
| العلاقة: | Report N°: RR-9448; hal-03526634; https://inria.hal.science/hal-03526634Test; https://inria.hal.science/hal-03526634v2/documentTest; https://inria.hal.science/hal-03526634v2/file/report.pdfTest |
| الإتاحة: | https://inria.hal.science/hal-03526634Test https://inria.hal.science/hal-03526634v2/documentTest https://inria.hal.science/hal-03526634v2/file/report.pdfTest |
| حقوق: | info:eu-repo/semantics/OpenAccess |
| رقم الانضمام: | edsbas.74F6D4AE |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |