Page 36 - profile-ok

研究群 ｜ Research Laboratories

Programming Languages and Formal Methods
程式語言與形式方法實驗室

Laboratory

研究人員 研究群介紹 Group Profile

莊庭瑞 Tyng-Ruey Chuang 程式語言研究形式語言使用於計算表達以及程式設計時的各種議題；形式方法泛指用於規 Research in programming languages investigates the syntactic, seman-
Associate Research Fellow 範、發展、及驗證軟體或硬體系統的數學方法與技術。兩者都強調其所使用方法的嚴謹性， tic, and pragmatic issues in the use of formal languages for expressing
Computer Science, New York University
以及所使用的方法是否可落實為軟體工具，被普遍使用。 computations and in programming machines. Formal methods are
王柏堯 Bow-Yaw Wang mathematically based techniques for the specification, development,
Associate Research Fellow 軟體系統在模組性與擴充性的研究議題，目前非常受到重視。一般認為，於程式設計或編 and verification of software and hardware systems. Formal methods and
Computer Science , University of Pennsylvania 譯時，若可以提早找出軟體於執行時可能發生的缺失，將可以大幅降低因軟體出錯而導致 programming languages both emphasize the rigidity of the methods
的損失。使用形式方法，來確保軟體正確性的作法，也日益普遍；而形式方法要能有效使
陳郁方 Yu-Fang Chen that are used. It is important that the methods are realized as software
Assistant Research Fellow 用在含有巨量程式碼的軟體系統上，也依靠此軟體的模組化特性，以及軟體所使用語言的 tools that can be systematically applied. The two research areas are
Information Management , National Taiwan 模組性建構。 closely related; they cross-fertilize each other.
Universality
我們以程式語言與形式方法的角度，提出先進的模組化方法，以描述並驗證使用者所提出的
穆信成 Shin-Cheng Mu 程式性質規範。目前的研究重點在於：一、以自動機為基礎的模型驗證；二、ML 程式語言 Our contributions to this area include developing new program con-
Assistant Research Fellow struction and verification techniques, building practical software tools,
Computing Laboratory , University of Oxford 的模組化驗證；三、模組化、可擴充之依賴型態程式設計典範；四、關於直觀規則語言之 and exploring new research directions. The two main thrusts of our re-
組合式分析。為此目的，我們與國內外的著名研究機構保持聯繫與合作。此外，為培育新 search are: 1) the interplay of model checking and theorem proving tech-
世代的研究人才，我們也持續辦理一年一度的「邏輯、語言與計算」暑期研習營 (Formosan niques in formal verification, especially in the development of effective
Summer School on Logic, Language, and Computation; http://flolac.iis.sinica.edu.tw/flolac10/)。
methods that combine the strengths of the two techniques; 2) program-
ming language based approaches to software correctness, in particular
in the use of expressive type systems and high-level module constructs
to assure desirable program properties.
Currently, our research focuses on the following: automated composi-
tional verification and automata-based model checking, module-level
verification for ML-like languages, modular and extensible paradigms for
dependent type programming, and compositional reasoning with intui-
tionistic regular languages.
The following are specific examples of our research. First, we have pro-
posed several approaches to improving automated compositional
verification, such as extending it to allow the verification of the liveness
property and proposing a new algorithm that guarantees finding the
minimal contextual assumption of an assume-guarantee rule. Second-
ly, we have used program derivation techniques to solve optimization
problems (finding, for example, the maximum density segments), as well
as developed a library encoding program derivation in dependent types,
which allows one to prove properties in an algebraic way and have these
properties verified by the type checker. Lastly, we have shown how ML-
like modules can be used to construct a class of extensible membership
functions for regular languages that are correct by design.
In addition to our research endeavors, a significant portion of our re-
sources are dedicated to community outreach. We maintain close con-
tacts with several well-known research groups abroad. In addition, we
have organized the yearly Formosan Summer School on Logic, Language,
and Computation (FLOLAC) since 2007 (for the 2010 edition, please see
http://flolac.iis.sinica.edu.tw/flolac10/). Because of FLOLAC, more and
more students in Taiwan have been encouraged to study and conduct
research in programming languages and formal methods.

36 37