周巢塵

周巢塵，中科院院士、計算機軟體專家。60年代末轉入信息處理系統，計算機操作系統及網路系統的研製。自70年代中期，致力於程序設計方法學的研究，特別是形式化方法的研究。形式化方法建立了軟體工程的數學基礎，倡導軟體設計和開發的嚴格方法及工具，以期軟體工程最終躋身於現代工程科學行列。形式化方法已逐漸被軟體工業界所採用，特別是用於嚴格安全系統的研製。80年代，主要從事分散式系統的研究。90年代，從事實時系統研究。2000年當選為第三世界科學院院士。1993年當選中國科學院院士（學部委員）。

1937年11月生於上海，1958年畢業於北京大學數學力學系，1967年研究生畢業於中國科學院計算技術研究所。1985年任博士生導師，1986年6月起任中國科學院軟體研究所研究員，1988年10月被授予“國家級有突出貢獻的中青年專家”稱號。1993年當選中國科學院院士，2000年當選第三世界科學院院士。1992年8月至1997年7月兼任聯合國大學國際軟體技術研究所首席研究員，1997年8月至2002年8月兼任該所所長。

2000年當選為第三世界科學院院士，計算機專家。現任中國科學院軟體研究所研究員、聯合國大學國際軟體技術研究所所長、中國科學院院士。其研究領域是軟體設計方法學，主要貢獻是有關分散式計算系統和實時計算系統的設計方法。1981年與英國同事合作提出了分散式計算系統正確性的組合式驗證方法。1991年與英國及丹麥科學家合作建立了實時計算系統設計的一種新穎的邏輯方法。1992年以來，一直在聯合國大學國際軟體技術研究所工作，1997年起任該所所長。這個所是聯合國在澳門設立的一個研究機構，致力於向發展中國家傳授先進軟體技術。自1992年以來，該所已培訓了200多位來自30多個國家的研究生和年輕科學家及工程師，在第三世界建立了廣泛聯繫。該所的研究成果也獲得國際公認，已成為國際知名的軟體技術研究中心。1958年畢業於北京大學數學力學系。

1967年研究生畢業於中國科學院計算技術研究所。中國科學院軟體研究所研究員，聯合國大學國際軟體技術研究所所長。研究生期間，研讀數理邏輯，師從胡世華院士。

他長期從事計算機科學理論方面的研究，在軟體形式化理論方面取得了具有國際水平的研究成果，在國內外有關學術刊物和會議上發表30餘篇論文和論著。他主要從事程序設計理論，特別是分散式程序設計理論和實時系統設計理論的研究。他在分散式程序設計理論方面的研究成果獲1987年度國家自然科學獎二等獎。而且提出的時段演算，為實時系統的形式化設計和驗證做出了開創性的工作，得到國際同行的公認，已經帶動了國際上二十幾個國家的科學家參與這一方面的研究。

周巢塵院士長期從事計算機科學理論的研究，在軟體形式化理論方面做出了系統的、創造性的工作，取得了具有國際先進水平的研究成果，是我國分散式程序設計理論研究的先驅者和開拓者之一；陸汝鈐院士則在知識工程和基於知識的軟體工程方面作了系統的、創造性的工作，也是我國該領域研究的開拓者。兩位院士和周龍驤研究員一起分析了國內外軟體產業發展的情況，結合聯信永益的軟體業務發展實際，認為聯信永益投身於軟體規模化開發並努力躋身於歐美軟體外包產業，是選擇了一個非常好的時機，希望聯信永益能以自己的身體力行，探索出一條中國軟體業的強大之路，並在政府有關部門和科研院所的支持與幫助下，逐漸成為中國民營軟體企業中從事歐美軟體外包業務的佼佼者。

長期從事計算機科學理論的研究，在軟體形式化理論方面做出了系統的、創造性的工作，取得了具有國際先進水平的研究成果。是我國分散式程序設計理論研究的先驅者和開拓者之一，學術造詣深厚，有多項創造性的成果。在程序設計理論，特別是“分散式程序設計理論”的研究方面有卓越成績，獲1987年國家自然科學二等獎。而且致力於時段演算(DurationCalculus)的研究，取得了豐富的成果，已經成為實時系統形式化領域中國際公認的新途徑。

計算機軟體專家，中國科學院院士、第三世界科學院院士、聯合國大學國際軟體技術研究所前任所長、中國科學院軟體研究所研究員、中國科學院成都計算所兼職研究員周巢塵院士，在“科學與中國”、四川青年創新論壇上作了題為“程序驗證——解決老問題的新方略”的報告。他在報告中簡單介紹程序斷言(Assertion)的概念，斷言方法在工業界的應用以及國際上的驗證編譯器(VerifyingCompiler)計劃，並對程序驗證和代數符號計算關係做了介紹，建議把我國的代數符號計算方面的傑出成就應用於程序驗證的研究。