آموزش مدل‌چک کردن با استفاده از SAT و SMT - آخرین آپدیت

سرفصل ها و درس ها

ارضای گزاره‌ای (SAT) Propositional Satisfiability (SAT)

• مقدمه‌ای بر مسئله ارضای بولی Introduction to Boolean Satisfiability Problem

• فرم نرمال عطفی (CNF) Conjunctive Normal Form (CNF)

• مفاهیم پایه حل مسئله بر اساس استدلال (Resolution) Basic Concepts of Resolution

• یافتن تخصیص‌های ارضا کننده Finding Satisfying Assignments

• مقدمه‌ای بر الگوریتم CDCL Introduction to the CDCL Algorithm

• مروری بر الگوریتم CDCL Overview of CDCL Algorithm

• تصویرسازی الگوریتم CDCL CDCL Illustration

• کمینه‌سازی بندهای آموخته شده Learned Clause Minimization

• مقدمه‌ای بر استنتاج سریع Fast Deduction - Introduction

• دو لیتِرال مطابقت داده شده Two Matched Literals

• محاسبه هسته‌های UNSAT: بخش اول Computing UNSAT Cores: Part 1

• محاسبه هسته‌های UNSAT: بخش دوم Computing UNSAT Cores: Part 2

• شمارش تخصیص‌های ارضا کننده: بخش اول Enumerating Satisfying Assignments: Part 1

• شمارش تخصیص‌های ارضا کننده: بخش دوم Enumerating Satisfying Assignments: Part 2

• شمارش تخصیص‌های ارضا کننده: بخش سوم Enumerating Satisfying Assignments: Part 3

• تبدیل تسایتین (Tseitin) Tseitin's Transformation

مدل‌چک کردن مبتنی بر SAT SAT-Based Model Checking

• مقدمه‌ای بر مدل‌چک کردن محدود (BMC) Introduction to Bounded Model Checking

• گردش کار پایه در BMC Basic BMC Workflow

• بازبینی نمایش نمادین سیستم‌های انتقال Symbolic Representation of Transition Systems: Refreshment

• کدگذاری نمادین BMC Symbolic Encoding of BMC

• مثالی از BMC نمادین Example of Symbolic BMC

• معناشناسی LTL محدود بدون حلقه Bounded LTL Semantics Without a Loop

• کدگذاری LTL در مسیر محدود بدون حلقه Encoding of LTL on Bounded Path Without a Loop

• کدگذاری LTL در مسیر محدود با حلقه Encoding of LTL on Bounded Path With a Loop

• آستانه‌های کامل بودن Completeness Thresholds

• نامتغیرهای استقرایی و K-Induction Inductive Invariants and K-Induction

• مدل‌چک کردن مبتنی بر درون‌یابی (Interpolation) Interpolation-Based Model Checking

• محاسبه Preimage با استفاده از شمارش SAT Preimage Computation Using SAT Enumeration

مقدمه‌ای بر ارضای تحت تئوری (SMT) Introduction to Satisfiability Modulo Theories (SMT)

• مقدمه‌ای بر حل مسائل SMT Introduction to SMT Solving

• رویکردهای حل مسائل SMT Approaches to SMT Solving

• معماری عمومی حل SMT تنبل (Lazy SMT) Generic Architecture of Lazy SMT Solving

• مثالی از حل مسئله SMT Example of SMT Solving

• ویژگی‌های حل SMT تنبل Features of Lazy SMT Solving

• مقدمه‌ای بر حل‌کننده SMT مدل Z3 Introduction to SMT Solver Z3

• مثالی از مدل‌چک کردن محدود با استفاده از Z3 An Example of Bounded Model Checking Using Z3

• مقدمه‌ای بر منطق اختلاف اعداد صحیح Introduction to Integer Difference Logic

• مثال: منطق اختلاف اعداد صحیح Example: Integer Difference Logic

• مقدمه‌ای بر محاسبات خطی اعداد صحیح Introduction to Linear Integer Arithmetic

• مثال: محاسبات خطی اعداد صحیح Example: Linear Integer Arithmetic

• مقدمه‌ای بر برابری و توابع تفسیر نشده Introduction to Equality and Uninterpreted Functions

• حل تئوری EUF EUF Theory Solving

• مقدمه‌ای بر تئوری آرایه‌ها Introduction to Theory of Arrays

• مثال: مقدمه‌ای بر تئوری آرایه‌ها Example: Introduction to Theory of Arrays

• مقدمه‌ای بر ترکیب تئوری‌ها Introduction to Combining Theories

• استفاده از Nelson-Oppen در تئوری‌های ترکیبی Applying Nelson-Oppen to Combined Theories

• ملاحظات کاربردی و بهینه‌سازی‌ها Practical Considerations and Optimizations