● 左起：Joseph Sifakis教授、Moshe Y. Vardi教授以及Giuseppe De Giacomo教授
今天，應信息學部軟件工程學院邀請，2007年圖靈獎獲得者Joseph Sifakis教授，美國科學院院士、美國工程院院士、歐洲科學院院士Moshe Y. Vardi教授和ACM會士、IEEE會士Giuseppe De Giacomo教授三位計算機時序邏輯研究領域的頂尖專家來到華東師大，對話信息學部師生，分享前沿理念，並將以華東師大榮譽教授的新身份，助力華東師大推動人工智能領域的創新發展。
“最強大腦”加盟華東師大
● 華東師大校長錢旭紅為Joseph Sifakis教授頒發榮譽教授聘書
● 華東師大校長錢旭紅為Moshe Y. Vardi教授頒發榮譽教授聘書
今天，Joseph Sifakis教授和Moshe Y. Vardi教授分別受聘華東師大榮譽教授。華東師大校長錢旭紅為兩位教授頒發聘書，贈送華東師大紀念書籤，並佩戴校徽。
兩位教授均表示，非常期待與華東師大在科學研究、成果轉化、人才培養等領域繼續深化合作。
華東師大校長錢旭紅表示，信息科學學科在華東師大發展中的重要性日益上升，學科影響力也在不斷增強，華東師大依託“智能+”行動計劃，整合優勢資源，組建了信息學部，以協同全校信息科學研究力量，促進學科交叉融合，推動信息科學學科高峰建設。他希望兩位榮譽教授能為華東師大信息科學學科的未來發展提供幫助與建議。
● Joseph Sifakis教授
Joseph Sifakis教授是法國國家科學研究中心研究總監、歐洲科學院院士、法國科學院院士、美國文理科學院院士、美國國家工程院院士。
他創建的Verimag實驗室(UJF/CNRS/INPG)以嵌入式系統著稱世界，他發明的“模型檢查”技術廣泛應用於工業界。
● Moshe Y. Vardi教授
Moshe Y. Vardi教授首次提出了線性時態邏輯和自動機語言表達能力等價，該結論如今已是主流驗證領域核心技術的理論基石。
他還和Giuseppe De Giacomo教授聯合提出了有限行為解釋下的線性時態邏輯，成功將線性時態邏輯應用到了人工智能領域。此外，兩人還開創性地利用線性時態邏輯綜合研究來解決機器人路徑規劃的問題。
華東師大的“老朋友”
三位專家均與華東師大有著長期的深入合作關係，在聯合科研、人才培養、成果轉化等合作領域已產出多項成果。
● 今年5月，Joseph Sifakis來華東師大作學術報告
Joseph Sifakis教授早在2004年就以學術交流的形式來訪過華東師大軟件學院；今年5月，他再訪華東師大，與師生暢談“自主系統”，並實地考察華東師範大學國家可信嵌入式軟件工程技術研究中心和上海工業控制系統安全創新功能型平臺，指導軟件學院科研基地的科研項目及產品。
● 今年5月，Joseph Sifakis與何積豐院士探討學術問題
● 今年5月，Joseph Sifakis與華東師大研究團隊開展學術研討
他與華東師大嵌入式軟件與系統系、上海工業控制系統安全創新功能型平臺的研究團隊已建立了常規化的合作交流，並已受聘成為上海工業控制系統安全創新功能型平臺的“首席科學顧問”，定期舉行每週一次的視頻會議，合作撰寫的文章也已投稿。
他表示：“下一步，我們將與上海工業控制系統安全創新功能型平臺合作，在形式化方法、工具應用、產學研一體化等方面開展全方位的合作，聯合推動華東師大在相關領域的科學研究及成果轉化。”
Moshe Y. Vardi教授與華東師大的合作已有12年曆史，至今聯合培養博士研究生2名、博士後研究生1名，累計發表合作論文20餘篇，其中10餘篇是CCF推薦B類以上論文，包括5篇CCF A類推薦論文。
他與華東師大科研團隊的合作研究在解決計算機自動化驗證和程序綜合中的關鍵問題中作出了突破性貢獻，研究成果也達到了國際一流水準。雙方的最新合作聚焦於硬件驗證和機器人路徑規劃兩大時下熱門的研究領域，“我們的目標是在未來5年內，將已有的理論研究成果應用到商業化的計算機硬件安全和人工智能安全領域。”Vardi教授說。
Giuseppe De Giacomo教授從2019年初開始與華東師大可信計算驗證團隊進行了線性時態邏輯可綜合的問題研究，該研究的成果可以用來解決人工智能中的機器人路徑規劃問題。
據悉，華東師大的一名博士畢業生即將前往Giacomo課題組，深入系統地從事人工智能領域的機器人路徑規劃方法研究。
麗娃河畔大師開講
Vardi在題為“程序驗證：半個世紀的年輪”的報告中，首先介紹了自省的可查詢動態系統這一在社會經濟環境的關鍵領域越來越受到推崇的系統，然後闡述了AI、形式化方法、數據庫、處理器等其他計算機科學領域的發展為自省的可查詢動態系統領域帶來的積極影響，以及開放性的挑戰，最後，他就如何解決這些問題提出了自己的建議。
● Giuseppe De Giacomo教授
Giacomo在題為“自省的可查詢動態系統”的報告中，沿著時間線索講述了近70年來程序驗證思想在學術界、工業界等領域的發展和影響，其中包含理論基礎，也涉及到了具體方法以及程序驗證的輔助工具，同時還列舉了形式化方法對程序進行驗證的多個具有代表性的實例。
他表示，雖然程序驗證思想及方法已經取得了巨大的進步，但仍有許多工作要做，“程序驗證夢”是個非常有價值的夢想。
● 學生提問交流
來源｜信息學部軟件工程學院
文｜符哲琦
圖｜符哲琦 王雨汀
閱讀更多 華東師範大學 的文章
