מידע כללי
הכרת שיטות שונות לאימות תכניות ביחס למפרטים נתונים. הקורס מורכב משני חלקים. החלק הראשון סוקר שיטות דדוקטיביות. החלק השני סוקר שיטות בדיקת מודל. גישה דדוקטיבית (תכניות קלט-פלט): נכונות חלקית ועצירה של תכניות תרשימי זרימה. הגישה המצרפית-נכונות חלקית ועצירה. גישת בדיקת-מודל (תכניות תגובתיות): לוגיקות טמפורליות פסוקיות ומבני קריפקה. בדיקת מודל CTL עם הוגנות. הצגת BDDS ושימושיהם. בדיקת מודל סימבולית מבוססת BDDS. בדיקת מודל סימבולית חסומה, מבוססת SAT. הכרה והפעלה של כלי תוכנה לבדיקת-מודל.
פקולטה: מדעי המחשב
|תואר ראשון
|תארים מתקדמים
מקצועות קדם
234292 - לוגיקה למדעי המחשב או 234293 - לוגיקה ותורת הקבוצות למדעי המחשב
ספרי המקצוע
- Database management systems - Ramakrishnan, Raghu.
- File structures : an analytic approach - Salzberg, Betty
- Tools and algorithms for the construction and analysis of systems : 5th international conference, TACAS '99, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS '99, Amsterdam, The Netherlands, March 22-28, 1999 : proceedings - TACAS '99
מידע סמסטריאלי
שעות שבועיות
3 נקודות אקדמיות • 2 שעות הרצאה • 1 שעות תרגול • 1 שעות פרוייקט
ניווט לדף המקצוע
אחראים
דר. ויזל יקיר
מבחנים
מועד א: 05-05-2024- אולמן 307. 502. 505. 506. 507.
קבוצות רישום
|
|
|
|
|
|
שעות שבועיות
3 נקודות אקדמיות • 2 שעות הרצאה • 1 שעות תרגול • 1 שעות פרוייקט
ניווט לדף המקצוע
אחראים
דר. ויזל יקיר
מבחנים
מועד א: 17-02-2023 מועד ב: 10-03-2023קבוצות רישום
|
|
|
|
|
|
שעות שבועיות
3 נקודות אקדמיות • 2 שעות הרצאה • 1 שעות תרגול • 1 שעות פרוייקט
ניווט לדף המקצוע
אחראים
דר. ויזל יקיר
מבחנים
מועד א: 08-02-2022 13:00 - 16:00- אולמן 602. 604. 605. 606. 607.
- טאוב 3. 4. 6.
- אולמן 310.
קבוצות רישום
|
|
|
|