בקורס זה אנחנו מתעניינים בהגדרה של שפות מידול (modeling languages) ובשימוש במודלים (models) בהנדסת תוכנה.   נתמקד בהגדרה ובחקירה של שפות מידול, ביחסים בין מודלים, ובשיטות פורמליות מתאימות שנעזרות בניתוח אוטומטי (SAT solvers, BDD-based symbolic algorithms) כדי לספק למהנדסים הפשטות (abstractions) וכלים להתמודדות עם האתגרים של התכנון, הבניה, ההרצה, הבדיקה, התחזוקה, והאבולוציה של מערכות תוכנה.

בין הנושאים שנלמד:

Defining the syntax and semantics of modeling languages
Applications of formal verification and synthesis
Specification mining and model inference

בין השפות שנלמד:

Alloy
Temporal logics and SMV
Various sub languages of the UML and their extensions (class diagrams, sequence diagrams etc.)   

הקורס מיועד לתלמידי תואר שני ושלישי ופתוח גם לתלמידי תואר ראשון.
דרישות קדם לתלמידי תואר ראשון: תוכנה 1 ומודלים.
קורסים קשורים ומומלצים: לוגיקה, אימות תוכנה וחומרה, בדיקות תוכנה, סמינר מחקר על כלי תוכנה מתקדמים (0368-5190).