2024年5月31日，由新疆師范高等�？茖W校主辦，中國計算機協會（CCF）形式化方法專委會走進高校、“數字新時代 信創筑未來”科學文化傳播研討會在新疆師范高等�？茖W校亞心校區舉行。來自西南大學、西北工業大學、華東師范大學、國防科技大學、中國科學院軟件所等單位CCF形式化方法專委會委員走進高校，帶來了五場精彩的學術報告。信息科學與技術學院以及職業教育學院的師生240余人參加了此次活動。
    此次研討會由中共中央組織部第11批援疆專家、湖南大學金融與統計學院教授、博士生導師、我�？蒲刑庁撠熑四咔嗌街鞒�。校黨委副書記、校長木開依•加爾肯別克同志致開幕辭，表達了對CCF形式化方法專委會的感謝，以及對專家親臨我校做學術報告的歡迎。隨后，CCF形式化方法專委會副主任董威教授代表專委會致辭，介紹了專委會的情況及此次活動的目的。

      
 
                  與會領導和專家合影

      
  
                   會議現場

    會上，國家特聘專家、西南大學計算機學院教授、博士生導師、西南大學軟件理論與系統團隊負責人、軟件研究與創新中心（RISE）主任劉志明做了題為《邏輯思維與計算思維并兼談機器智能的能力》的主旨發言。他深入探討了數理邏輯，計算理論和程序語言的基本概念和思想，揭示數理邏輯是計算機科學和系統的天然基礎，通過數理邏輯，計算模型和程序語言的統一性理論，淺談在推理和思維中自然語言的局限性和符號化形式語言的必要性，基于哥德爾不完備定理，從哲學層面說明人的心智和人工智能（AI）能力范圍的區別。盡管AI取得了顯著進展，但也不具備類似于物理學中牛頓定律的科學基礎。他認為，目前人類的心智和意識仍然是獨特的，并且在可預見的未來，AI不太可能具有人類的心智能力。隨著技術的發展，人類將逐步建立AI的科學基礎，解答AI的能力范圍、可解釋性以及AI是否具備推理和規劃能力等問題。自然，與其他科技一樣，AI具有廣泛且強大的有益于人類的能力和作用，但如果使用不當，同樣也可能給人類帶來廣泛且嚴重的破壞。

      
 
                   劉志明教授作報告

    西北工業大學軟件學院教授，博士生導師， IEEE高級會員、可靠性性協會執委會委員（2018-2020）、西安分會主席，CCF杰出會員董云衛教授做了題為《智能軟件工程理論概述》的報告，介紹了以大語言模型為代表的生成式神經元網絡技術的快速發展和逐步應用，軟件開發模式也發生了巨大的變化，對軟件理論和工程實踐技術迎來巨大的變革和前所未有的挑戰，傳統軟件開發技術將被替代，軟件工程師的能力培養和工作角色也將發生巨大變革。依據軟件技術方法發展脈絡，介紹不同階段軟件開發技術及其形態的演化過程。重點介紹了基于深度學習軟件智能化開發方法的內涵及其技術思想，軟件開發流程及其活動。最后討論了智能軟件工程教育面臨的一些技術挑戰和熱點問題，并對軟件工程學科技術發展趨勢進行展望。

       
 
                    董云衛教授作報告

    中共中央組織部第11批援疆專家、華東師范大學軟件工程學院副教授、CCF嵌入式專委會、形式化方法專委會委員郭建做題為《基于PC-ABAC模型的Linux安全文件系統》的報告，介紹了隨著信息技術的高速發展，數據和資源的規模呈現爆發式增長，安全性逐漸成為信息系統領域的重要主題。訪問控制機制被認為是保證數據共享和系統安全性的一項重要手段，針對基于屬性訪問控制實施過程中出現的問題，介紹了基于策略限制的屬性訪問控制（PC-ABAC）的形式化模型，通過對屬性和訪問控制策略的形式化定義，結合滿足性理論，利用求解器對屬性和策略進行安全性驗證。在 Linux 文件系統中部署PC-ABAC 模型，實現了對 Linux 文件系統的安全訪問控制。

       
 
                    郭建副教授作報告

    國防科技大學計算機學院教授、博士生導師、CCF形式化方法專委會副主任董威教授的“人機物融合計算技術及應用”報告，介紹了人機物融合系統已被認為是未來信息系統發展的主要形態，軟件是三元融合的核心，“軟件定義一切”已成為趨勢。探討了人機物融合計算中人機物融合系統的發展歷程和特點，介紹了體系架構、系統建模、代碼生成、驗證等技術，以及人機物融合系統在多個領域的應用前景。

      
 
                    董威教授作報告

    中國科學院軟件研究所基礎軟件與系統重點實驗室（計算機科學國家重點實驗室）研究員，博士生導師、CCF形式化方法專委會秘書長吳志林就《計算機軟硬件基礎設施的形式化驗證》進行了深入的報告，介紹了一種基于數學推理的驗證計算機系統的理論和方法——形式化方法。形式化驗證技術是采用邏輯推理的手段來保障計算機系統的正確性與安全性，已經廣泛用于計算機軟硬件基礎設施的驗證，包括芯片設計、操作系統與編譯器、網絡與分布式協議等。介紹了計算機軟硬件基礎設施的形式化驗證國內外相關工作，以及對形式化方法在未來的應用進行了展望。

      
 
                   吳志林教授作報告

    在互動交流環節，與會專家與我校師生進行了熱烈的討論與交流，為師生的學術研究與教育實踐提供了寶貴的指導。最后，信息科學與技術學院宋彬院長對本次研討會進行總結，并對參與本次研討會的專家學者再次表達了誠摯的感謝。
    本次研討會由中共中央組織部第11批援疆專家、華東師范大學軟件工程學院副教授、CCF嵌入式專委會、形式化方法專委會委員郭建策劃發起，為我校師生近距離接觸國內高水平大學及科研院所的專家提供了非常好的交流平臺，促進了我校師生了解國內外在形式化方法、人工智能、大模型等領域的最新發展，推動了我校學術水平的提高。 （楊瑞紅）

來源：產新網