10月16日下午，應計算機科學國家重點實驗室的邀請，美國新墨西哥大學Deepak Kapur教授到軟件所進行學術交流，并作題為Automatic Generation of Program Invariants from Traces的學術報告。報告會由張健研究員主持。 

報告中，Deepak Kapur教授針對程序循環不變式的自動生成問題進行了系統介紹。循環不變式生成是形式驗證中的關鍵問題，難度很大。Kapur教授介紹了他和他的博士生Thanh Vu Nguyen提出的一種新的循環不變式生成方法，該方法可發現非線性以及含有數組表達式的循環不變式。報告結束后，與會人員就形式驗證和軟件工程領域的一些熱點問題與Kapur教授進行了深入廣泛的交流。 

Deepak Kapur教授現任美國新墨西哥大學計算機科學系杰出教授。他得到中國科學院“外國專家特聘研究員”項目支持，在中國科學院軟件研究所訪問九個月。他的研究領域包括自動推理、符號計算、形式化方法。他長期擔任Journal of Symbolic Computation，Journal of Automated Reasoning等相關領域國際主流雜志的編委（其中1993至2007年擔任Journal of Automated Reasoning主編）；曾獲得自動推理界最高獎-- Herbrand獎。

Deepak Kapur教授作報告