גרא וייס

תכנות התנהגותי והרכבת התנהגויות

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

מאמר היסוד, Communications of the ACM, 2012 · המאמר על BPjs

דרישות חיות ושיטות פורמליות

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

Keeping Behavioral Programs Alive, 2024. מאמר המשך: Adding liveness to behavioral programming: theory, implementation, and user study, Requirements Engineering, 2025.

בינה מלאכותית בפיתוח תוכנה

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

יצירת קוד התואם לדרישות, REW 2024 · BPpy, ENASE 2025

הבנת תקלות ובדיקות מבוססות מודלים

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

Automata Models for Effective Bug Pattern Description, MODELS 2025

כריית תהליכים

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

Guarded Process Trees, ICPM 2025

אלגוריתמים הסתברותיים ותכנון תחת אי־ודאות

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

Efficient optimal Kolmogorov approximation of random variables, Artificial Intelligence, 2024

קומבינטוריקה ומשחקים

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

De Bruijn Sequences: from Games to Shift-Rules to a Proof of the Fredricksen-Kessler-Maiorana Theorem, 2025

ראייה ממוחשבת וניתוח תנועה

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

Human pose estimation for automated biomechanical swimming analysis, Sports Biomechanics, 2026 (in press)

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

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

הגישה המחקרית מתוארת במאמר Provengo: A Tool Suite for Scenario Driven Model-Based Testing, המציג בנייה הדרגתית של מודלי בדיקה מתוך תרחישים.

אתר החברה · המאמר על Provengo

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

מבוא ללוגיקה

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

מבוא לאימות תוכנה בשיטות פורמליות

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

סילבוס לדוגמה

חידות סייבר

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

קטלוג הקורסים של האוניברסיטה

EasyLean — הוכחות באמצעות בלוקים

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

פתיחת ההדגמה · קוד המקור

סימולטור שערים לוגיים

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

פתיחת הסימולטור · קוד המקור

קטלוג תרחישי דיבוג בתכנות התנהגותי

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

לצפייה בקטלוג

פרויקטים במימון הקרן הלאומית למדע המופיעים בפרופיל המחקר:

פרסומים

רשימת הפרסומים המלאה זמינה ב־CRIS וב־DBLP. עמודי תחומי המחקר לעיל מפנים למבחר עבודות יסוד ועבודות מהשנים האחרונות.

קשר

דוא״ל אקדמי: geraw@bgu.ac.il. פרטי המשרד, הטלפון ושעות הקבלה נמצאים ב־פרופיל הסגל הרשמי.