توصیف و وارسی برنامه‌ها
Program Specification and Verification
| مقطع: تحصیلات تکمیلی | گرایش: نرم‌افزار |
| نوع درس: نظری | تعداد واحد: ۳ |
| پیش‌نیاز: – | هم‌نیاز: – |
هدف کلی
این درس مقدمه‌ای بر توصیف عملکرد برنامه‌ها با منطق و تئوری و ساخت وارسی‌کننده‌های برنامه است. این درس فنون قدرتمند برای استدلال صوری درباره برنامه‌ها و مجموعه ابزارهای نوین در این زمینه را پوشش می‌دهد. دانشجویان مهارت‌های لازم را برای طراحی، توسعه، و به‌کارگیری ابزارهای وارسی‌کننده که وارسی پیمانه‌ای برنامه‌های پیچیده را امکان‌پذیر می‌سازد به دست خواهند آورد. علاوه بر این، دانشجویان انواع مختلفی از اصول پایه‌ای استدلال و چگونگی به‌کارگیری این اصول از طریق ابزارهای خودکار را فرا می‌گیرند.
سرفصل‌ها
- روش‌های مبتنی بر منطق ریاضی برای توصیف کارکرد صحیح برنامه‌ها
- مبانی استدلال منطقی
- حل‌کننده‌های SMT برای استدلال خودکار درباره فرمول‌های منطق
- زبان‌های میانی وارسی (مثل Viper) برای مدل‌سازی روش‌های وارسی
- وارسی حلقه‌ها و رویه‌ها
- وارسی ویژگی‌های چالش‌برانگیز برنامه‌ها (مثل مدیریت پویای حافظه)
- وارسی برنامه‌های همروند
ارزیابی پیشنهادی
- آزمون میان ترم: ۳۰ درصد نمره
- آزمون پایان ترم: ۳۰ درصد نمره
- انجام تکلیف‌های عملی و پروژه درس: ۴۰ درصد نمره
منابع پیشنهادی
- F. Nielson and H. Riis Nielson. Formal Methods: An Appetizer. Springer International Publishing, 2019.
- B.C. Pierce et al. Software Foundations. Published online: https://softwarefoundations.cis.upenn.edu, last accessed 2024.