冰島雷克雅未克大學Luca Aceto和Anna Ingolfsdottir教授到軟件所交流
文章來源: | 發布時間:2013-11-28 | 【打印】 【關閉】
11月13日-26日,冰島雷克雅未克大學Luca Aceto和Anna Ingolfsdottir教授應計算機科學國家重點實驗室的邀請到軟件所進行學術交流,并作學術報告。報告會由林惠民院士主持。
11月21日,Luca Aceto教授在5號樓334報告廳進行了題為Rule Formats for Structural Operational Semantics: A Very Short Introduction的學術報告。操作語義通過程序在抽象機器上的執行來描述程序的行為。結構化操作語義是給出程序設計和規約語言操作語義的一種語法驅動、基于規則的方法。報告中,Luca Aceto教授介紹了其研究團隊在結構化操作語義理論方面的成果,改研究的目的在于用純粹語法的方法保證程序和規約語言滿足某些合意的語義性質。規則格式是推理規則所需要滿足的語法模板,只要操作語義的推導規則滿足一定的格式,就可以保證所定義的語義具有相應的性質。報告會上,Luca Aceto教授還對規則格式作了詳細的闡述。
11月25日,Anna Ingolfsdottir教授在5號樓334報告廳進行了學術報告,報告的題目為Towards model checking the hardware description language BSV。報告中,Anna Ingolfsdotti教授首先由淺入深地闡述了對硬件描述語言BSV的驗證方法,BSV是一種可直接編譯為硬件代碼的面向對象語言。隨后,Anna Ingolfsdotti教授介紹了其研究團隊將BSV翻譯到實時系統描述語言Uppaal上的初步工作,這一工作使得在生成最終硬件產品之前對BSV設計進行模型檢測成為可能。
兩場報告會十分精彩。報告會后,與會人員就規則格式、SBSV和Uppaal如何轉換、轉換是否保持判定性等問題與兩位教授進行了深入交流。
Luca Aceto教授現為冰島雷克雅未克大學計算機科學學院教授,他是歐洲理論計算機科學學會(EATCS)的現任主席。他目前致力于并發語義、計算機科學邏輯、結構化操作語義、驗證問題和生物信息學問題的計算復雜性等方面的研究。
Anna Ingolfsdottir教授現為冰島雷克雅未克大學計算機科學學院教授,主要從事并發理論及其在軟件開發中的應用、生物學中的數學和計算建模等方面的研究。