سنتز نرم‌افزار
Software Synthesis
| مقطع: تحصیلات تکمیلی | گرایش: نرم‌افزار |
| نوع درس: نظری | تعداد واحد: ۳ |
| پیش‌نیاز: – | هم‌نیاز: – |
هدف کلی
سنتز نرم‌افزار به مجموعه روش‌ها و الگوریتم‌هایی اطلاق می‌شود که از توصیف برنامه مورد نظر، متن کد برنامه را تولید می‌کنند. سنتز نرم‌افزار یک دانش میان‌رشته‌ای است. تکنیک‌های سنتز از یک سو با اتکا به مبانی ریاضی زبان‌های برنامه‌سازی و از سوی دیگر بر مبنای الگوریتم‌های هوش مصنوعی کار می‌کنند. یکی از اهداف مهم سنتز یاری رساندن به افرادی است که تخصص برنامه‌نویسی ندارند. این افراد با ارائه توصیف‌های سطح بالا نظیر مثال‌هایی برای رفتار برنامه، می‌توانند ایجاد برنامه جدید کنند. دانشجویان در این درس با حیطه‌های کلاسیک و جدید نظیر برنامه‌نویسی با مثال، سنتز حل محدودیت توسط ابزار SMT solver، سنتز با کمک انواع، سنتز در علوم داده و سنتز با کمک شبکه‌های عصبی آشنا می‌شوند.
سرفصل‌ها
- مقدمه‌ای بر سنتز استقرایی (جستجوی شمارشی از پایین به بالا، بالا به پایین)
- مدل‌های آماری در سنتز
- جستجوی تصادفی
- جستجوی مبتنی بر نماینده‌های فضای حالت
- مساله صدق‌پذیری بولی (SAT) و صدق‌پذیری در پیمانه نظریات
- سنتز مبتنی بر محدودیت با طرح
- مقدمه‌ای بر سنتز عملکردی
- از درستی‌سنجی تا سنتز
- سنتز با انواع پالایش
- سنتز استنتاجی (deductive)
- سنتز برای علم داده
- یادگیری مدل
ارزیابی پیشنهادی
- فعالیت‌های کلاسی در طول نیم‌سال: ۶۰ درصد نمره
- آزمون پایان نیم‌سال: ۴۰ درصد نمره
منابع پیشنهادی
- A. Solar-Lezama. Introduction to Program Synthesis. MIT, 2018.
- S. Gulwani, O. Polozov, and R. Singh. Program Synthesis. Now Foundations and Trends, 2017.
- B. C. Pierce et al.. Software Foundations. https://softwarefoundations.cis.upenn.edu/, University of Pennsylvania, 2024.