Page 37 - profile2014.indd
P. 37
程式語言與形式方法實驗室
局部推理中之合成問題。當有很多可行的局部屬性，演算式 對並行程式而言，由於各個線程交織之行為，造成要被探索
學習可以有效率地推斷出其中之一。除此之外，學習型合成 之狀態空間非常之大。為了有效地探索狀態空間，採用抽象
演算法在推斷屬性之形式上，給我們更多彈性。這些彈性將 技術是必須的。我們計劃結合現有並行程式之抽象化技術。
幫助我們了解有關程式之局部屬性。 例如，線程模組化抽象以簡化控制部分，而謂詞抽象以簡化
數據部分。我們的目標是規模化並行軟體模型檢測，以驗證
對一般的程式開發者而言，由於缺乏訓練，運用形式化技術 無法以現有方式處理之程式。
可能並不切實際。然而，愈來愈多的並行程式正由一般的程
式開發者所發展。並行程式之驗證工具無疑地將幫助程式開 除了我們的研究活動外，我們同時也奉獻顯著的資源於教
發者提高他們的生產力。現有並行程式的一大部分，是由 育。為了介紹我們的研究給學生，我們自 2007 年以來，每
C++ 和 Java 等現代程式語言所編寫而成。為了這些現有的 年舉辦「台灣邏輯，語言和計算暑期學校 (FLOLAC) 」。藉
程式，我們還打算開發自動驗證方法，以保證其正確性。準 由 FLOLAC，鼓勵越來越多的台灣學生至程式語言和形式方
確地說，我們打算開發並行軟體模型檢測方法。而模型檢測 法此一領域，學習並進行研究。
之核心技術，則是高效率地探索欲驗證程式的狀態空間。
37
