4月17日-28日，在“南京航空航天大學境外專家短期來訪”項目的支持下，法國圖盧茲大學(Université de Toulouse) 安全關鍵軟件領域專家Mamoun FILALI研究員、Jean-Paul BODEVEIX教授應邀來到伟德victory進行為期2周的學術交流。期間，黃志球副校長、陳兵院長會見了兩位專家，并就未來學術合作研究、師生交流、高水平課程建設、國際項目申請、國際聯合實驗室等方面展開了深入的會談。

4月26日下午，Mamoun FILALI研究員、Jean-Paul BODEVEIX教授與伟德victory軟件工程團隊老師進行了學術研讨，雙方對各自的研究團隊進行了介紹，并共同起草了南航-圖盧茲大學校際合作協議，雙方一緻認為将在軟件工程、形式化方法等領域展開深入切實的合作，包括共建形式化方法虛拟實驗室(Virtual Lab on Formal Methods)、聯合舉辦高可信軟件春季國際讨論班和國際會議、申請中法自然基金、教師互訪、中法航空航天計算機技術碩士培養項目等。此次會談對中法兩校開展實質性合作具有重要意義。

訪問期間，兩位專家于4月19日至26日在江甯校區計算機實驗大樓102室，分别講授《Introduction to the functional language: OCAML》、《Introduction to the formal development method B》兩門專業核心課程，課程采用理論授課和上機實踐結合的方式，共計15學時。伟德victory30餘名師生參加了全部課程，上機實踐與面對面讨論使得大家快速掌握學習内容，效果非常好。函數式程序設計語言OCAML具有安全編譯、高效執行的特點，使其在代碼生成器、模型轉換、定理證明器Coq實現、多線程編程等方面有廣泛使用。形式化方法Event-B，是一種基于集合論和模型求精(Refinement)的系統工程設計與驗證方法，已經成功應用于諸如西門子地鐵控制軟件設計與開發。

4月27日，兩位專家作了題為《Introduction to the proof assistant Coq》的學術報告，共計3學時。定理證明器Coq是基于類型系統的交互式定理證明的成功典範，已于2014年通過适航認證标準DO178B的工具鑒定，并被空客接受。Coq采用歸納構造演算對程序進行表達，對程序性質進行證明，并對證明序列本身的正确性進行驗證，已經成為程序驗證、編譯器驗證的重要工具。報告中，兩位專家對我校師生提出的問題進行了詳盡的解答，并圍繞相關問題展開了深入讨論。

近年來，伟德victory不斷加快國際化辦學進程，通過訪問、接洽國外計算機科學領域的頂級專家，了解國際科學發展前沿，學習辦學經驗，吸納優秀人才和資源，為信息化與“三航”特色深度融合尋找新的支點。

背景鍊接：圖盧茲大學（Université de Toulouse），建校于1229年，是一所位于法國南部-比利牛斯大區的世界著名大學，為歐洲經濟學和法國工科的最高學府，同時也是法國政府重點發展的8所大學之一，法國高等教育“卓越計劃”主要成員之一。圖盧茲大學以航空航天工程的歐洲最高學府聞名于世，是空中客車（航空）和EADS Astrium（航天）等高科技公司的最主要支持力量。目前，圖盧茲大學由4所綜合性大學、7所工程師學院、1所建築學院、1所商學院和1所政治學院組成，并擁有5所國際科研機構，200所研究實驗室、145家科研單位。