جدول پیوندها
1 مقدمه
2 لینک رقص
3 زبان برنامه نویسی Rust
4 RAC: تضمین مشترک سخت افزار/نرم افزار در مقیاس
5 زنگ و RAR
5.1 زنگ الگوریتمی محدود
6 پیوند رقص در Rust و 6.1 تعاریف
6.2 ترجمه به ACL2
6.3 قضایای پیوندهای رقص
7 کارهای مرتبط
8 نتیجه گیری
9 قدردانی و مراجع
تعدادی از زبانهای دامنه خاص که هم اجرای سختافزار و هم نرمافزار را هدف قرار میدهند و برای تأیید رسمی پشتیبانی میکنند، ایجاد شدهاند. کریپتول [5]به عنوان مثال، به عنوان یک «مشخصات طلایی» برای ارزیابی پیادهسازیهای رمزنگاری استفاده شده است، که در آن ابزارهای خودکار بررسی هم ارزی را بین مشخصات Cryptol برای یک الگوریتم معین و اجرای VHDL انجام میدهند.
سیستم های تایید رسمی برای Rust شامل Creusot است [8]، بر اساس WhyML; پروستی [3]، بر اساس زنجیره ابزار تأیید Viper. و RustHorn [20]، بر اساس بندهای هورن محدود شده است. AWS در حال توسعه یک بررسی کننده مدل برای Rust، Kani است [2]. علاوه بر این، دانشگاه کارنگی ملون در حال توسعه Verus است، یک ابزار مبتنی بر SMT برای تأیید رسمی برنامههای Rust. [19]. با Verus، برنامه نویسان اثبات ها و مشخصات را با استفاده از نحو Rust بیان می کنند، که به اثبات ها اجازه می دهد از انواع خطی Rust و بررسی قرض گرفتن استفاده کنند. جالب خواهد بود که انواع آن را امتحان کنید …