A software tool for representing and checking Sokoban solutions using Formal Verification

הרקע לפרויקט:

שיטות של אימות פורמלי מאפשרות להוכיח נכונות של מערכות תוכנה וחומרה מורכבות. כלי האימות מאפשרים לסרוק ולנתח מרחב מצבים גדול. יכולות אלה ניתן ליישם לפתרון בעיות שונות, כולל משחקים מרחביים.

מטרת הפרויקט:

מטרת הפרויקט לפתח כלי מבוסס אימות פורמלי (Formal Verification) לייצוג משחק Sokoban שהוא משחק מאתגר לפתרון ממוחשב. הכלי יאפשר ייצוג של בעיות Sokoban ווריאציות שלהן ובדיקה של פתרונות לבעיות אלה.

תכולת הפרויקט:

במהלך הפרויקט הסטודנטים ירכשו ידע בשיטות אימות פורמלי וסינתזה (Formal Verification and Synthesis) וייפתחו ויבדקו כלי תוכנה לייצוג למשחקים מרחביים כולל Sokoban . הכלי יאפשר לנהל תחרות בין אלגוריתמים שונים ובדיקה יעילה של הפתרונות.

קורסי קדם:

83691 Formal Verification and Synthesis

מקורות:

1. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).
2. https://www.mathsisfun.com/games/sokoban.html