10月28日，高可信軟件應(yīng)用技術(shù)研討會在安徽合肥召開。本次會議由中國科學(xué)技術(shù)大學(xué)計算機學(xué)院、中國科大-國創(chuàng)高可信軟件工程中心主辦；【科大國創(chuàng)(300520)、股吧】（300520）及其控股子公司安徽中科國創(chuàng)高可信軟件有限公司承辦，會上發(fā)布了高可信軟件驗證平臺（學(xué)習(xí)版），標(biāo)志著驗證工具走向?qū)嵱没?，也為一下步商業(yè)化奠定了基礎(chǔ)。

　　在“軟件定義一切”的時代，未來社會經(jīng)濟高質(zhì)量的發(fā)展，都離不開軟件技術(shù)的支撐。特別是在航空航天、國防裝備、核能、金融、醫(yī)療設(shè)備、交通等安全攸關(guān)的應(yīng)用領(lǐng)域，開發(fā)高可信的軟件成為迫切的需求。

　　科大國創(chuàng)起源于中科大，中科大為公司信息技術(shù)產(chǎn)品研發(fā)與整體解決方案提供技術(shù)和人才支撐。2008年中科大與耶魯大學(xué)聯(lián)合成立中科大-耶魯高可信軟件聯(lián)合研究中心，合作開展對于高可信軟件和形式化驗證各個領(lǐng)域的研究；2014年，科大國創(chuàng)與中科大共建軟件工程中心，組建了高可信軟件研究技術(shù)團(tuán)隊，希望逐步研發(fā)出有市場前景的高可信軟件開發(fā)方法、技術(shù)和工具等；在此基礎(chǔ)上，2017年兩家又共同出資成立了中科國創(chuàng)高可信軟件有限公司，經(jīng)過2年多的發(fā)展，在操作系統(tǒng)、關(guān)鍵算法的形式化驗證、程序驗證工具和程序靜態(tài)分析等方面擁有諸多理論突破和研究成果，并擁有基于這些理論建立的程序驗證與分析框架和程序驗證技術(shù)。

　　本次研討會上展示了高可信軟件的生態(tài)體系。這是一款程序驗證的學(xué)習(xí)平臺，具有世界領(lǐng)先水平的高可信軟件開發(fā)工具產(chǎn)品及技術(shù)，打造以程序分析和程序驗證為核心的高可信軟件集成開發(fā)平臺，標(biāo)志著科大國創(chuàng)領(lǐng)先的高可信軟件技術(shù)已走出開發(fā)間，技術(shù)成果已嶄露頭角，為進(jìn)一步的規(guī)模市場化應(yīng)用奠定了堅實的基礎(chǔ)。

　　據(jù)悉，為普及程序形式化驗證的基礎(chǔ)蒞臨、方法和技術(shù)，中科國創(chuàng)高可信將舉辦首期“程序驗證入門培訓(xùn)班”，采用講解和實踐相結(jié)合的學(xué)習(xí)方式，幫助軟件技術(shù)人員掌握基本的程序驗證技術(shù)。（胡心宇）