Verifying annotated program families using symbolic game semantics

در این مقاله، یک رویکرد مبتنی بر معناشناسی بازی کارآمد برای تأیید خانوادههای برنامه باز، یعنی خانوادههای برنامه با اجزای نامشخص (شناسهها) پیشنهاد می کنیم. ما از نمادگرایی معانی الگوریتمی بازی استفاده می کنیم، که در آن مقادیر نمادین برای ورودی به جای آن از بتن استفاده می شود. به این ترتیب، ما می توانیم به طور فشرده ارائه خانواده های برنامه با عدد صحیح نامحدود به عنوان به نام (حالت محدود) اتوماتیک نماد برجسته است. سپس الگوریتم های مدل سازی طراحی شده به طور خاص، به طور یکنواخت، ایمنی تمام برنامه ها (انواع) را از یک خانواده به طور همزمان با استفاده از یک مدل جمع و جور و برای مشخص کردن برنامه هایی که نا امن هستند (به ترتیب بی خطر) مورد استفاده قرار می گیرند. ما یک نمونه اولیه از این رویکرد را ارائه می دهیم و کاربرد آن را با چند نمونه نشان می دهیم.