Page 34 - profile2012.indd
P. 34

Research Laboratories  研究群



                                                                                                                                                          程式語言與形式方法實驗室


                Programming Languages




                                  and Formal Methods                                                                                  Laboratory




          研究人員


             王柏堯 Bow-Yaw Wang          莊庭瑞 Tyng-Ruey Chuang     陳郁方 Yu-Fang Chen          穆信成 Shin-Cheng Mu
             Associate Research Fellow  Associate Research Fellow  Assistant Research Fellow   Assistant Research Fellow



               研究群介紹


             程式語言與形式方法實驗室發展保證程式正確性之技術。                           統表達能力上之限制，這些實現仍然遠遠落後於現在理論                                            對一般的程式開發者而言，由於缺乏訓練，運用形式化技術可能並不切
             我們在程式語言方面的研究，著重於發展正確程式之語                            上之發展。我們計劃將會話型別嵌入到  Agda  ķ  一個具有                                     實際。然而，愈來愈多的並行程式正由一般的程式開發者所發展。並行
             法、語意、及實務上之議題；在形式方法方面的研究，強                           豐富的依賴型別系統之程式語言。希望建立一個程式開發                                            程式之驗證工具無疑地將幫助程式開發者提高他們的生產力。現有並行
             調分析真實程式中演算法、計算、以及實際方面之課題。                           者寫作Agda/Haskell程式之綜合性環境，並使用型別系統                                      程式的一大部分，是由 C++  和 Java  等現代程式語言所編寫而成。為
             我們應用數學及形式技術，以探討我們的研究問題。我們                           以保證正確性及終止性。                                                          了這些現有的程式，我們還打算開發自動驗證方法，以保證其正確性。                                     為了幫助程式開發者充分
             亦致力於發展工具及方法論，以幫助程式開發者寫作正確                                                                                                準確地說，我們打算開發並行軟體模型檢測方法。而模型檢測之核心技                                     利用並行處理器之計算能
             程式。                                                 我們對於以「證明即程式」方式達到程式正確性要求的程                                            術，則是高效率地探索欲驗證程式的狀態空間。
                                                                 式設計方法與工具（如jCoq），深感到興趣，將探究這                                                                                                               力，本實驗室致力於並行
             多核處理器現在被廣泛使用於桌上電腦、筆記型電腦、甚                           類工具的細節、功能以及限制。我們選定了三項應用領域                                            對並行程式而言，由於各個線程交織之行為，造成要被探索之狀態空間
             至是智慧型手機。程式開發者自然想要利用並行性，以提                           的題目為作為研習的標的：一、正規表達式的導數，二、                                            非常之大。為了有效地探索狀態空間，採用抽象技術是必須的。我們計                                     程式之語言與驗證技術。
             昇應用程式之效率。但是並行程                                                         結構化內容的轉換，三、軟體元件                                   劃結合現有並行程式之抽象化技術。例如，線程模組化抽象以簡化控制
             式寫作卻相當困難。就算是有經                                                         間的互動。這三項應用領域內的題                                   部分，而謂詞抽象以簡化數據部分。我們的目標是規模化並行軟體模型
             驗的程式開發者，也會在寫作並                                                         目，與一般應用程式的開發與正確                                   檢測，以驗證無法以現有方式處理之程式。
             行程式時出錯。因此，雖然並行                                                         性，有相當關聯。例如，網頁程式
             電腦已廣為普及，並行程式之數                                                         是否能安全執行、正確輸出、以及                                   除了我們的研究活動外，我們同時也奉獻顯著的資源於教育。為了介紹
             量仍非常地有限。為了要幫助程                                                         良好互動，分別和以上一、二、三                                   我們的研究給學生，我們自2007年以來，每年舉辦「台灣邏輯，語言和
             式開發者利用現今處理器之計算                                                         項應用領域中的一些問題相關。                                    計算暑期學校(FLOLAC)」。藉由FLOLAC，鼓勵越來越多的台灣學生至
             能力，程式語言與形式方法實驗                                                                                                           程式語言和形式方法此一領域，學習並進行研究。
             室故致力於並行程式之語言與驗                                                         模型檢測是一種指認程式設計錯誤
             證技術。                                                                   之 技 術 。 給 定 一 個 有 關 設 計 的 屬
                                                                                    性，模型檢測工具藉由搜索設計行
             型別系統已廣泛地應用於現代程                                                         為，以決定性地驗證給定之屬性。
             式語言，以確保型別安全。舉例                                                         對 並 行 系 統 而 言 ， 設 計 的 行 為 與
             而言，一個型別不良運算式可能會將數字0和字元’0’相加，                        設計組件之數量成指數增長。這是眾所周知的狀態爆炸問
             而產生一個不正確的結果。型別系統允許程式開發者，在                           題。局部推理是一種為減緩在驗證並行系統中狀態爆炸問
             編譯時就能指認此類型別錯誤。並行程式寫作易出錯已廣                           題，所發展之組合分析技術。異於探索全局之狀態，此組
             為人知。而程式開發者的挑戰，在現今由數百甚至數千交                           合技術合成局部屬性，並在設計組件中驗證這些屬性。除
             互溝通線程所組成之程式下，更形艱鉅。現代程式語言便                           了古典有限並行程式，局部推理亦被用來分析參數系統。
             採用型別系統，以保證程式中某類性質。
                                                                 局部屬性之合成，是局部推理成功的關鍵。傳統上，局部
             「會話型別」是一個為傳遞消息並行系統所發展之型別系                           屬性乃由定點計算獲得。然而，迭代計算可能是不必要的
             統，它能確保線程之間的溝通遵循某些協議。較先進的變                           昂貴。我們計劃將演算式學習，應用於在局部推理中之合
             化也能保證無死鎖。現在已做了些努力，藉由嵌入到現有                           成問題。當有很多可行的局部屬 性，演算式學習可以有效
             程式語言，以實現會話型別。不過，由於宿主語言型別系                           率地推斷出其中之一。除此之外，學習型合成演算法在推
                                                                 斷屬性之形式上，給我們更多彈性。這些彈性將幫助我們
                                                                 了解有關程式之局部屬性。





               研究群
         34    Research Laboratories
                                                                                                                                                                                                                                            35
   29   30   31   32   33   34   35   36   37   38   39