פרויקטי גמר שנה"ל תשע"ט - הנדסת מחשבים

101 Parallel Computation of Distance Maps

חישוב מקבילי של מפות מרחקים

שם המנחה: דר' אופיר וובר

אחראי אקדמי: דר' אופיר וובר 

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

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

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

דרישות:

• יכולת תכנות טובה.
• עיבוד דיגיטלי של גיאומטריה 83-656-01  ניתן לקחת במקביל.
• חישוב מקבילי ב GPU83-920-01. לא חובה אך יתרון. ניתן לקחת במקביל.
• יכולת עבודה עצמאית והגדלת ראש.

מקורות: http://www.eng.biu.ac.il/~weberof/Publications/PMM/SIGGRAPH08.zip                   

102 Geometric Deep Learning

למידה גיאומטרית עמוקה

שם המנחה: דר' אופיר וובר 

אחראי אקדמי: דר' אופיר וובר 

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

בעשור האחרון חלה התפתחות מרעישה בתחום של לימדת מכונה ובעיקר זו המבוססת על רשתות נוירונים בעלות מספר רב של שכבות. בולטות במיוחד הן ארכיטקטורות המבוססות על רשתות קונבולוציה (Convolutional Neural Network) שהתפתחו יד ביד עם התפתחות חומרה גרפית מקבילית (GPU) המאפשרת עיבוד וחישוב מסיבי בזמן יחסית קצר. אלה הביאו לפריצות דרך משמעותיות בתחומים כמו ראייה ממוחשבת על ידי בניית אלגוריתמי סיווג והבנה סמנטית של תמונות.

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

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

דרישות מקורות:

• יכולת תכנות טובה. ידע ב Matlab, Python - יתרון.
• עיבוד דיגיטלי של גיאומטריה (83-656-01). ניתן לקחת במקביל.
• רקע בסיסי בתחום של למידה עמוקה.
• יכולת עבודה עצמאית והגדלת ראש.

מקורות: http://geometricdeeplearning.com/    

103 Images Come to Life

תמונות מתעוררות לחיים

שם המנחה: דר' אופיר וובר

אחראי אקדמי: דר' אופיר וובר

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

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

דרישות מוקדמות:

• עיבוד דיגיטלי של גיאומטריה (83-656-01). ניתן לקחת במקביל.
• תכנות C++.
• יכולת עבודה עצמאית והגדלת ראש.

דוגמא לשם המחשה של ממשק המשתמש:

http://www-ui.is.s.u-tokyo.ac.jp/~takeo/research/rigid/index.html

דוגמא לאלגוריתם מתקדם לביצוע המניפולציה של התמונה:

https://www.youtube.com/watch?v=6ZdGQmqR45Q&feature=youtu.be

104 Implementation and Analysis of high-rate interactive coding schemes against erasure noise

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

שם המנחה: דר' רן גלס

אחראי אקדמי: דר' רן גלס 

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

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

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

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

1. לימוד רקע תיאורטי על קידוד פרוטוקולים אינטראקטיביים
2. מימוש בתוכנה של סכמה קידוד תקשורת אינטראקטיבית מתקדמת (לפי מאמר מס׳ 1 במקורות הרצ״ב)
3. ביצוע סימולציית רעש ומדידת איכות הקידוד המתקבל (הסתברות הצלחה, קצב הקוד כפונקציה של הרעש, וכו׳)

המימוש יבוצע בשפה עילית כלשהי (C, ג׳אווה, פייתון וכו׳) על גבי מחשב יחיד שידמה את שני המחשבים המתקשרים ואת ערוץ התקשורת ביניהם.

דרישות:

• מבוא לתורת הצפינה (מקביל)
• נושאים מתקדמים בפרוטוקולים אינטראקטיביים (יתרון)

מקורות:

• Capacity of Interactive Communication over Erasure Channels and Channels with Feedback.R. Gelles and B. Haeupler. SIAM Journal on computing, 2017
• Coding for Interactive Communication: A Survey. R. Gelles. Foundations and Trends in Theoretical Computer Science, 2017.http://www.eng.biu.ac.il/~gellesr/survey.pdf 

105 A web-based system for finding (lost) forked crypto-coins

פיתוח מערכת web להצלת מטבעות קריפטוגרפיים מפוצלים

שם המנחה: דר' רן גלס

אחראי אקדמי: דר' רן גלס 

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

טכנולוגיית ה-BlockChain מאפשרת מימוש מטבע ״דיגיטלי״ (דוגמת מטבע ביטקוין – bitcoin) בצורה מבוזרת מעל האינטרנט, וללא צורך בבנק מרכזי. חברי רשת הבלוקציין שומרים על פעילותה ואוכפים את חוקיה ע״י תהליך של כריית מטבעות – תהליך שמגדיר איך מוסיפים בלוק חדש לשרשרת הבלוקים הקיימת. כאשר יש אי-הסכמה בקהילה, קורה לעיתים שחלק מהכורים ״משנים את החוקים״ ומתחילים לייצר שרשרת נוספת הפועלת במקביל לשרשרת המקורית. תהליך זה נקרא פיצול או Fork.
לאחר הפיצול נוצרים למעשה ״שני״ מטבעות שונים, שלהם היסטוריה משותפת. בפרט, כל מטבע שהיה קיים לפני הפיצול ישוכפל ויתקיים בשתי השרשראות השונות. דוגמא לפיצול כנ״ל הוא BitCoin Cash שהתפצל ממטבע הBitcoin.

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

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

הפרויקט הינו פרויקט פיתוח תוכנה ומצריך ידע בפיתוח תוכנה ופיתוח ל-web.
תהליך הפרויקט יורכב מהשלבים הבאים:

1. למידת נושא ה-Bitcoin והבנת טכנולוגיית BlockChain.
2. למידת נושא הפיצולים וההיסטוריה של מטבעות שפוצלו מרשת ה-bitcoin.
3. פיתוח אתר אינטרנט לאיתור מטבעות מפוצלים אבודים
4. בדיקת האתר על רשת הביטקוין האמיתית

דרישות:

הנדסת תוכנה
ידע קודם בפיתוח ל-web – יתרון. אחרת ייתכן שיידרש קורס משלים ממדמ״ח (למשל 89541) 

מקורות:

• Bitcoin and Cryptocurrency Technologies. A. Narayannan, J. Bonneau, E. Felten, A. Miller and S. Goldfeder, Princeton Press, 2016.
• The Internet

106 Formal Verification of Protocols for Pedestrians and Autonomous vehicles

מידול ואימות פורמלי של פרוטוקול השתלבות של הולכי רגל בנתיב תחבורה של רכבים אוטונומיים

שם המנחה: דר' הלל קוגלר

אחראי אקדמי: דר' הלל קוגלר

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

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

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

דרישות:

• 83691 Formal Verification and Synthesis (במקביל לפרויקט)
• 83869 Cyber Physical Systems (במקביל לפרויקט)

מקורות:

1. Althoff, Matthias, et al. "Safety verification of autonomous vehicles for coordinated evasive maneuvers." Intelligent vehicles symposium (IV), 2010 IEEE. IEEE, 2010
2. Loos, Sarah M., André Platzer, and Ligia Nistor. "Adaptive cruise control: Hybrid, distributed, and now formally verified." FM 2011: Formal Methods. Springer Berlin Heidelberg, 2011. 42-56.
3. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).
4. Nilsson, Petter, et al. "Preliminary results on correct-by-construction control software synthesis for adaptive cruise control." Decision and Control (CDC), 2014 IEEE 53rd Annual Conference on. IEEE, 2014. 

107 Algorithmic solution of mathematical riddles

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

שם המנחה: דר' הלל קוגלר

אחראי אקדמי: דר' הלל קוגלר

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

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

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

1. https://www.logic-puzzles.org/init.php
2. https://www.brainzilla.com/logic/zebra/who-owns-the-crocodile/
3. http://matchstickpuzzles.blogspot.co.il/

דרישות:

83691 Formal Verification and Synthesis (במקביל לפרויקט)

מקורות:

1. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).
2. Federico Chesani, Paola Mello, Michela Milano. Solving Mathematical Puzzles: A Challenging Competition for AI. Association for the Advancement of Artificial Intelligence, 2017.  

108 Theory of Network Based Biocomputation

תאוריה של חישוב ביולוגי מקבילי

שם המנחה: דר' הלל קוגלר

אחראי אקדמי: דר' הלל קוגלר

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

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

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

דרישות:

83670 Biological Computation (במקביל לפרויקט)
83691 Formal Verification and Synthesis (במקביל לפרויקט)

מקורות:

1. Nicolau, Dan V., et al. "Parallel computation with molecular-motor-propelled agents in nanofabricated networks." Proceedings of the National Academy of Sciences, 2016.
2. http://bio4comp.org/

109 Online Algorithms for Budgeted Maximum Coverage

אלגוריתמים מקוונים לכיסוי מקסימום מתוקצב

שם המנחה: דר' דרור רביץ

אחראי אקדמי: דר' דרור רביץ 

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

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

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

דרישות:

קורסי קדם: מבני נתונים ואלגוריתמים 2, אלגוריתמים מקוונים.

מקורות:

1. A. Borodin and R. El-Yaniv. Online Computation and Competitive Analysis. Cambridge University Press, 1998.
2. B. Saha and L. Getoor. On Maximum Coverage in the Streaming Model & Application to Multi-topic Blig Watch. In SDM, 697-708, 2009.
3. G. Ausiello, N. Boria, A. Giannakos, G. Lucarelli, V. Th. Paschos. Online maximum k-coverage. Discrete Applied Mathematics 160(13-14):1901-1913, 2012.
4. D. Rawitz and A. Rosén. Online budgeted maximum coverage. In 24th ESA, LIPIcs 57, 73:1-73:17, 2016

110 Non-uniform multi-coverage in Client-Server Networks

כיסוי מרובה לא אחיד ברשתות לקוח-שרת

שם המנחה: דר' דרור רביץ

אחראי אקדמי: דר' דרור רביץ 

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

הפרוייקט יעסוק בבעייה של הקצאת משאבים במערכת שכוללת שרתים שמשרתים לקוחות. המערכת כוללת קבוצת שרתים בעלי קיבול חסום, וקבוצת לקוחות כאשר לכל לקוח יש דרישה למשאב, ורווח שהוא מוכן לשלם רק בתנאי שדרישתו תסופק במלואה. לכל לקוח נתונה תת קבוצה של שרתים שיכולים לשרת אותו (השייכות לקבוצה זו יכולה להיות קשורה, למשל, למיקום גיאוגרפי). כמו כן, השירות שלקוח מקבל מהשרתים אינו אחיד. פתרון הוא התאמה בין לקוחות למשאבי הספקים כך שמתקיים: (1) לקוח מקבל משאבים רק משרתים שנמצאים בתת הקבוצה שלו, ו- (2) סך הדרישות שמשוייכות לשרת לא עולה על הקיבול שלו. מותר ללקוח לקבל שירות מיותר משרת אחד. המטרה היא למצוא פתרון שמביא למקסימום את הרווח הכולל של לקוחות שדרישותיהם מסופקות במלואן. הבעיה הנ"ל ממדלת הקצאת רוחב פס ברשתות סלולריות דור 4. במסגרת הפרוייקט הסטודנטים ילמדו על אלגוריתמי קירוב לפתרון הבעיה והכללות שלה, ויבחנו את ביצועיהם. בפרט, ביצועי האלגוריתמים יושוו לאלגורימים נאיביים ולביצועים שמובטחים מהניתוח התיאורטי שלהם.

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

דרישות:

קדם: מבני נתונים ואלגוריתמים 2, תורת הגרפים ושימושיה, אלגוריתמים מקוונים.

מקורות:

1. D. B. Shmoys and E. Tardos. An approximation algorithm for the generalized assignment problem. Mathematical Programming 62:461-474, 1993.
2. C. Chekuri and S. Khanna. A polynomial time approximation scheme for the multiple knapsack problem. SIAM Journal on Computing 35(3):713-728, 2006.
3. D. Amzallag, R. Bar-Yehuda, D. Raz, G. Scalosub. Cell selection in 4G cellular networks. IEEE Transactions on Mobile Computing 12(7): 1443-1455, 2013.
4. O. Gurewitz, Y. Sandomirsky, and G. Scalosub. Cellular Multi-Coverage with Non-uniform Rates. 33rd INFOCOM, 1330-1338, 2014.

111 Identifying critical events in biological networks using time and clocks

זיהוי אירועים קריטיים ברשתות ביולוגיות באמצעות שיטות של זמן ושעונים

המנחים: פרופ' צבי לוטקר, דר' הלל קוגלר

אחראים אקדמים : פרופ' צבי לוטקר, דר' הלל קוגלר

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

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

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

דרישות:

83670 Biological Computation (במקביל לפרויקט)

מקורות:

1. Lotker, Zvi. "The tale of two clocks." Advances in Social Networks Analysis and Mining (ASONAM), 2016 IEEE/ACM International Conference on. IEEE, 2016.
2. B. Yordanov, S-J Dunn, H Kugler, A. Smith, G. Martello and S. Emmott, S. A Method to Identify and Analyze Biological Programs through Automated Reasoning, Nature Systems Biology and Applications, 2016.

112 Algorithms for solving linear programs of bounded dimension

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

המנחים: פרופ' צבי לוטקר, דר' דרור רביץ

אחראים אקדמים : פרופ' צבי לוטקר, דר' דרור רביץ 

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

תכנות לינארי (Linear Programming) הוא אחד מהכלים המרכזיים בפיתוח וניתוח אלגוריתמים. ידועים אלגוריתמים לפתרון תוכניות לינאריות בזמן פולינומי, אך זמן הריצה של האלגוריתמים הללו עדיין כבד. בפרוייקט זה נתמקד בתוכניות לינאריות במימד חסום, כלומר עם מס' קבוע של משתנים, אך מספר לא חסום של אילוצים. נלמד על אלגוריתם לפתרון תכנות לינארי במימד חסום וננסה להאיץ את זמן הריצה שלהם ע"י שימוש באקראיות ובמיקבול.
במסגרת הפרוייקט הסטודנטים ילמדו רקע תיאורטי על תכנות לינארי במימד חסום ועל אלגוריתמים לפתרון הבעיה. לאחר מכן הסטודנטים יבחנו את ביצועי האלגוריתמים באמצעות מימושם. ביצועי האלגוריתמים יושוו לביצועים שמובטחים מהניתוח התיאורטי שלהם, ולביצועי אלגוריתמים ידועים.

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

דרישות:

קורסי קדם: מבני נתונים ואלגוריתמים 2, אופטימיזציה רציפה וקומבינטורית.

מקורות:

1. M. de Berg, O. Cheong, M. van Kreveld, M. Overmars. Computational Geometry: Algorithms and Applications. Third edition. Springer, Berlin, Heidelberg, 2008.
2. J. Matousek, M. Sharir, and E.Welzl. A subexponential bound for linear programming. Algorithmica 16(4-5): 498-516, 1996.

113 Micro architectural features based on machine learning

מיקרו-ארכיטקטורה של מעבד מבוססת למידת מכונה

המנחים: בנימין פרנקל

אחראים אקדמים : פרופ' שמואל וימר

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

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

בפרויקט זה, נרצה להשתמש באלגוריתמים קיימים של למידת מכונה לצורך שיפור ביצועי המעבד. מטרת הפרויקט היא לממש חזאי קפיצות (Branch Predictor) המבוסס על טכנולוגיית Machine Learning עבור מעבד מצונר, ולהטמיע אותו במעבד קיים תוך מימוש חומרתי של החזאי.

במסגרת הפרוייקט הסטודנטים ילמדו רקע תיאורטי על אלגוריתמי למידת מכונה, ויתאימו אלגוריתם רלוונטי לצורך Branch Prediction . לאחר מכן הסטודנטים יבחנו את ביצועי האלגוריתם באמצעות מימושו. ביצועי החזאי יושוו לביצועי חזאים ידועים קלאסיים. הסטודנטים יטמיעו את החזאי במימוש חומרתי בשפת SystemVerilog בתוך מעבד מחקרי קיים (PULP) ויבחנו את ביצועי המעבד עם החזאי החדש.

דרישות:

קורסי קדם הנדרשים לביצוע הפרויקט:

• תכן לוגי
• מבנה מחשבים ספרתיים
• תכן חומרה בשפת Verilog.

מקורות:

https://www.pulp-platform.org/

Jiménez, D. A., & Lin, C. (2001). Dynamic branch prediction with perceptrons. In High-Performance Computer Architecture, 2001. HPCA. The Seventh International Symposium on (pp. 197-206). IEEE.‏

114 Deeply fused pipelined dot product multiplier

מכפל מהותך מצונר

המנחים: בנימין פרנקל

אחראים אקדמים : פרופ' שמואל וימר

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

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

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

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

דרישות:

• שליטה ב C++/C וידע או נכונות ללמידת JAVA.
• תיתכן קישוריות מסויימת לעיבוד המבוצע במטלב.

דרישות קורסים:

• רשתות מחשבים ואינטרנט 1 (83455) -נדרש
• תכנות מונחה עצמים (83233) - נדרש
• קורס עיבוד אות - יתרון
• סדנת אנדרואיד - יתרון

מקורות:

http://www.eng.biu.ac.il/~wimers/files/conferences/21-ASAP2016.pdf

115 Network-based Audio Control and Distribution Center

מרכז בקרת אודיו מבוסס רשת

המנחים: פיני טנדייטניק

אחראים אקדמים : דר' רן גלס 

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

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

• מחשבים ניידים
• מכשירי אנדרואיד
• DSP BOARD
• TI WiFi Audio Device
• Raspberry Pi

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

כל אחד מהמקורות לעיל מייצר זרם של מידע אותו נרצה לרכז במחשב רשתי שיהווה ״מרכז בקרה והפצה של אודיו״ ויאפשר למשל עיבוד, שמירה off-line או הפצה on-line של המידע המגיע מהמקורות השונים אל לקוחות המעוניינים לקבל את המידע (המעובד).

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

דרישות:

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

מקורות:

1. https://en.wikipedia.org/wiki/Broadcasting
2. Cross-correlations for determining the time delay between two signals (https://en.wikipedia.org/wiki/Cross-correlation#Time_delay_analysis )
3. https://www.mathworks.com/help/signal/ref/finddelay.html
4. RASPBERRY PI 3 MODEL B+ : https://en.wikipedia.org/wiki/Cross-correlation#Time_delay_analysis
5. SimpleLink Wi-Fi CC3200 LaunchPad , http://www.ti.com/tool/cc3200-launchxl

116 Synthesis from Temporal Logic Specifications

אלגוריתמים לסינתזה מאפיון דרישות בלוגיקת הזמן

המנחים: דר' הלל קוגלר

אחראים אקדמים : דר' הלל קוגלר

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

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

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

דרישות:

83691 Formal Verification and Synthesis (במקביל לפרויקט)

מקורות:

1. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995). 
2. A. Pnueli and R. Rosner "On the synthesis of a reactive module". POPL '89 Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Pages 179-190, 1989. 
3. S. Jacobs et al. "The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results." (2017): 116-143.

טופס ההרשמה במסלול הנדסת מחשבים