Program Specification and Verification
| مقطع: تحصیلات تکمیلی | گرایش: نرم‌افزار |
| نوع درس: نظری | تعداد واحد: ۳ |
| پیش‌نیاز: – | هم‌نیاز: – |
این درس مقدمه‌ای بر توصیف عملکرد برنامه‌ها با منطق و تئوری و ساخت وارسی‌کننده‌های برنامه است. این درس فنون قدرتمند برای استدلال صوری درباره برنامه‌ها و مجموعه ابزارهای نوین در این زمینه را پوشش می‌دهد. دانشجویان مهارت‌های لازم را برای طراحی، توسعه، و به‌کارگیری ابزارهای وارسی‌کننده که وارسی پیمانه‌ای برنامه‌های پیچیده را امکان‌پذیر می‌سازد به دست خواهند آورد. علاوه بر این، دانشجویان انواع مختلفی از اصول پایه‌ای استدلال و چگونگی به‌کارگیری این اصول از طریق ابزارهای خودکار را فرا می‌گیرند.