圖靈獎得主Clarke教授訪問中國科大蘇州研究院

2020-12-04 中國科學院

　　10月20日至27日，美國卡內基梅隆大學計算機系教授、中國科學院「愛因斯坦講席教授」、圖靈獎得主Edmund Clarke對中國科學技術大學蘇州研究院進行了為期8天的學術訪問與交流。

　　21日上午，Clarke教授為蘇州研究院的師生帶來了題為Model Checking and the Curse of Dimensionality的精彩報告。Clarke教授在演講中回顧了模型檢查理論技術的發展歷程，分析了在過去20多年裡面遇到的四個典型的難題，講解了科研人員如何解決這些難題並取得重大突破。

　　22日上午，Clarke教授為中科大-耶魯高可信軟體聯合研究中心師生作題為Symbolic Model Checking with BDDs的講座，深入淺出地介紹了符號化模型檢查的由來與基本算法原理，還興致勃勃地講述了在1992年他與他的學生們採用該模型檢查算法檢測到一個緩存一致性協議存在缺陷的故事，這一協議來自一個當時已經公布四年之久的工業標準協議（IEEE FutureBus+ Standard）。這是第一個採用形式化方法在IEEE標準中找到錯誤的應用案例，展現了模型檢查方法在工業硬體設計領域中的應用前景。

　　23日上午，Clarke教授為研究中心師生帶來了第二場專場講座，題目為Bounded Model Checking with SAT/SMT。Clarke教授在這個講座中重點講述了他在模型檢查方法中取得的一個重大突破——目前已在工業界廣泛採用的基於SAT工具的限界模型檢查方法。研究中心的師生表示通過這個內容詳實的講座學習到了模型檢查最前沿的研究成果與工業應用，收穫頗豐。

　　隨後的幾天裡，Clarke教授與研究院的師生進行了面對面的深入交流，並聽取了中科大-耶魯高可信軟體聯合研究中心、嵌入式系統實驗室等團隊的工作介紹。Clarke教授對中國科大蘇州研究院各團隊的研究課題表示出了極大的興趣，並提出了寶貴意見。

　　Edmund Clarke教授是形式化驗證領域中模型檢查技術的創始人之一，美國計算機學會（ACM）與美國電氣電子工程師學會（IEEE）Fellow，同時也是美國國家科學院和工程院院士。Clarke教授於2007年和另外兩位科學家E．Allen Emerson和Joseph Sifakis一同分享了「圖靈獎」，以表彰他們對模型檢查理論與技術做出的奠基性貢獻。目前模型檢查技術已成為一個被廣泛應用在硬體和軟體工業中非常有效的驗證技術。

相關焦點

  • CNCC首批KN講者：圖靈獎得主、院士、名企專家將做特邀報告
    首批特邀講者官宣確認，圖靈獎得主、院士、名企專家將在CNCC2020做特邀報告。CNCC2020首批特邀報告講者確認，其中包括：ACM圖靈獎獲得者John Hennessy、中國工程院院士廖湘科、中國工程院院士李培根、中國科學院院士劉明，
  • 菲爾茲獎得主Efim Zelmanov受可瀚學堂創始人邀請訪問中國科大
    Efim Zelmanov教授在可瀚學堂董事長何海平的多次邀請下，於12月13日至15日，對中國科學技術大學（以下簡稱「中國科大」）展開了為期三天的訪問，作為教授多年的好朋友，何海平全程陪同。包校長熱誠邀請教授常來訪問，共同探討雙方進一步的科研合作。Efim Zelmanov教授在校領導的陪同下參觀了中國科大校史館。青藤掩映的中國科大校史館外觀雖不起眼，館內卻別有洞天，有「兩彈一星功勳獎章」、中國第一臺質子靜電加速器等"鎮館之寶"；還有郭沫若任校長時的辦公桌等極富文物價值的實物、以及國際頂尖的科研成果。中國科大短暫卻厚重的歷史、卓越的教學與科研成就讓教授為之讚嘆。
  • 特邀報告丨圖靈獎得主John E. Hopcroft教授
    10月16日，由中國人工智慧學會、重慶市人工智慧學會主辦，重慶郵電大學、科大訊飛股份有限公司承辦的「2020大數據智能化發展暨人工智慧創新發展高峰論壇之信息科技前沿論壇」在重慶郵電大學成功召開。圖靈獎得主、美國科學院/美國工程院/美國藝術與科學院院士、中國科學院外籍院士、美國康奈爾大學John E.
  • 這7位圖靈獎得主
    這7位圖靈獎得主，竟然今日才入選ACM Fellow，他們可是程式設計師「祖師爺」7位圖靈獎得主計算機科學許多基礎研究的關鍵是ACM研究員。要知道，ACM—美國計算機協會是世界著名的重要計算機組織，會員是其重要榮譽之一。計算機領域的諾貝爾獎由ACM頒發。今天（2021年1月14日），當ACM新選出的研究員名單公布時，七位靈魂獎得主的名單令人驚訝。
  • 國際著名數學家、菲爾茲獎得主丘成桐教授訪問我校並做客「大師...
    2019年12月28日，應我校邀請，國際著名數學家、菲爾茲獎得主丘成桐教授訪問我校並做客中國科大「大師論壇」，以「數學歷史大綱」為題為全校師生做精彩報告。本次報告會在東區理化大樓東三報告廳舉行，並在西三報告廳進行實況轉播。
  • 72歲圖靈獎得主姚期智院士創業,建立南京圖靈AI研究院
    雷鋒網獲悉，4月20日，計算機科學最高獎圖靈獎唯一華裔得主（截至2017年）、中科院院士姚期智率領清華團隊組建新型研發機構——南京圖靈人工智慧研究院。南京市委書記張敬華親自出席了研究院揭牌與項目籤約儀式。姚期智於2000年獲得計算機科學領域最高獎圖靈獎。
  • 圖靈獎得主Edmund Clarke因新冠逝世
    據最新消息，2007年圖靈獎得主、計算機科學家Edmund Clarke，因感染新冠肺炎，於北京時間12月23日上午不幸逝世。7年後，也就是1989年，Edmund 被任命為正教授。2007年，他與Ernest Allen Emerson和Joseph Sifakis一起，因在模型檢查方面取得的傑出貢獻而獲得圖靈獎。
  • 華人著名計算機科學家劉炯朗逝世，圖靈獎得主姚期智為其得意門生
    圖靈獎唯一華人得主姚期智為其得意門生。消息稱，臺灣清華大學前校長劉炯朗7日因病過世，享壽86歲。現為集邦科技股份有限公司董事長、香港城市大學訪問學者、國立成功大學電機工程學系李國鼎科技講座教授與國立清華大學蒙民偉榮譽講座教授。
  • 華人著名計算機科學家劉炯朗逝世,圖靈獎得主姚期智為其得意...
    圖靈獎唯一華人得主姚期智為其得意門生。 消息稱，臺灣清華大學前校長劉炯朗7日因病過世，享壽86歲。，2000年時當選中央研究院院士。 現為集邦科技股份有限公司董事長、香港城市大學訪問學者、國立成功大學電機工程學系李國鼎科技講座教授與國立清華大學蒙民偉榮譽講座教授。
  • 7位圖靈獎得主當選,新晉多位華人,2020 ACM Fellow公布
    在 95 名入選者中，包括多位華人，如杜克大學教授陳怡然、浙大教授任奎等，更有多名圖靈獎得主當選，可謂星光熠熠。姓名：呂晨陽機構：聖路易斯華盛頓大學當選理由：因對自適應實時系統、實時虛擬化和無線網絡物理系統的貢獻當選個人介紹：呂晨陽是中科大少年班傑出校友，現為美國聖路易斯華盛頓大學計算機科學與工程系教授、IEEE Fellow，研究興趣包括實時系統、無線傳感器網絡和信息物理融合系統。
  • 中國科大蘇州高等研究院生物醫學工程學科建設研討會順利舉行
    10月20日下午，中國科大蘇州高等研究院召開生物醫學工程學科建設研討會，中國科大黨委常委、副校長杜江峰院士通過網絡視頻主持大會。中國科大黨委常委褚家如教授，中科院蘇州醫工所黨委書記楊洪波研究員，教育部生物醫學工程類教學指導委員會委員史國權研究員，中國科大人力資源部部長薛天教授，美國醫學與生物工程院和英國皇家化學學會Fellow潘挺睿教授，美國醫學與生物醫學院Fellow周少華教授，以及北京大學、清華大學、浙江大學、北京航空航天大學、中科院上海微系統與信息技術研究所、中科院蘇州納米所等單位的領導專家出席會議。
  • 圖靈獎得主 Edmund Clarke 因感染「新冠」逝世
    Clarke 在社交媒體發布了一封訃告稱，他的父親、2007 年圖靈獎得主 Edmund M. Clarke 因感染新冠肺炎不幸去世，享年 75 歲。2007 年度圖靈獎被授予給了 Edmund M.之後，Clarke 教授在杜克大學任教兩年後，於 1978 年加入哈佛大學並擔任助理教授。1981年，他與自己的博士生 Allen Emerson 首次提出了模型檢測的想法並用在自動機並發系統的驗證研究上，成為形式邏輯研究方面模型檢查的開創者之一。1982 年，他加入了卡內基梅隆大學計算機系，並於 1989 年被評為全職終身教授一職。
  • 又一位巨星因「新冠」隕落,圖靈獎得主Edmund Clarke,享年75歲
    據最新消息，2007年圖靈獎得主、計算機科學家Edmund Clarke，因感染新冠肺炎，於北京時間12月23日上午不幸逝世。其子James S. Clarke在Twitter發文公布此消息之餘，也悼念道：雖然他對（我）學業上的成功總是抱有很高的期望，但他也教會了我打棒球、釣魚和環遊世界。我將深深地懷念他。
  • 他是圖靈獎唯一華人得主,更是中國人工智慧引路人
    姚期智是哈佛大學的物理學博士，師從諾貝爾物理學獎得主格拉肖（Sheldon Lee Glashow）。但在太太儲楓的影響下，他轉投計算機領域，最終憑藉對計算理論，包括偽隨機數生成、密碼學與通信複雜度作出的突出貢獻，獲得圖靈獎。功成名就之後，姚期智回到中國任教，並重新加入中國國籍。
  • 19位諾貝爾獎、圖靈獎及菲爾茲獎得主
    19位諾貝爾獎、圖靈獎、菲爾茲獎得主，以及7位中國科學院、中國工程院、國際歐亞科學院院士匯聚山城，展開一場精彩的智慧碰撞。 　　此次峰會是2019智博會重要活動之一，由重慶市人民政府主辦，重慶市科學技術局、重慶兩江新區管理委員會承辦，上海交通大學科學技術發展研究院協辦。
  • A.M.圖靈獎獲得者、CMU教授Edmund M. Clarke因COVID去世
    據外媒報導，卡內基梅隆大學(CMU)名譽教授、A.M. 圖靈獎得主Edmund M. Clarke在長期患病後於當地時間周二死於COVID-19，享年75歲。Clarke來自黎巴嫩山，他最著名的工作成果是模型檢查，這是一種檢測計算機硬體和軟體設計錯誤的自動化方法。
  • 【蘇州新聞】中國科大蘇州高等研究院第一屆理事會第一次會議召開
    【蘇州新聞】中國科大蘇州高等研究院第一屆理事會第一次會議召開 11月26日，中國科學技術大學蘇州高等研究院第一屆理事會第一次會議召開
  • 近日，蘇州大學2位教授當選歐洲科學院院士！
    8月26日，蘇州大學轉化醫學研究院院長、蘇州大學附屬第一醫院副院長時玉舫收到歐洲科學院院長發來的賀信，祝賀他當選歐洲科學院院士。8月29日，隨著名單公布，又一喜訊傳來，蘇州大學功能納米與軟物質研究院教授遲力峰當選歐洲科學院外籍院士。
  • 2007年圖靈獎得主Edmund Clarke因感染新冠離世...
    而前幾天，讓計算機圈子格外惋惜的是，當地時間12月22日，2007年圖靈獎得主，美國著名計算機專家，愛德蒙·克拉克（Edmund M. Clarke）因感染新冠肺炎不幸去世，享年75歲。2007年，克拉克教授與艾倫·愛默生教授（Allen Emerson）和約瑟夫·斯發基斯（Joseph Sifakis）共同獲得有著計算科學領域諾貝爾之稱的圖靈獎。獲獎理由是他們開發的模型檢測技術，成為一個廣泛應用在硬體和軟體工業中非常有效的算法驗證技術。
  • A.M.圖靈獎獲得者、CMU教授Edmund M. Clarke因COVID-19去世
    據外媒報導，卡內基梅隆大學(CMU)名譽教授、A.M. 圖靈獎得主Edmund M. Clarke在長期患病後於當地時間周二死於COVID-19，享年75歲。Clarke來自黎巴嫩山，他最著名的工作成果是模型檢查，這是一種檢測計算機硬體和軟體設計錯誤的自動化方法。