Page 37 - profile2012.indd

Research Laboratories 研究群

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

Programming Languages

and Formal Methods Laboratory

Research Faculty
Research Faculty

Bow-Yaw Wang Yu-Fang Chen Tyng-Ruey Chuang Shin-Cheng Mu
Associate Research Fellow Assistant Research Fellow Associate Research Fellow Assistant Research Fellow

Group Profile

The Programming Languages and Formal Methods research “Session type” is a type system for message-passing concurrent all design behaviors. For concurrent systems, the number of design behaviors
group develops techniques for ensuring program correctness. programs that ensures that communication between threads grows exponentially in the number of design components. This is the infa-
Our researches in programming languages focus on the syntac- follow certain protocol. More advanced variations also guaran- mous state explosion problem. Local reasoning is a compositional technique
tic, semantic, and pragmatic issues in the development of cor- tee deadlock-freeness. Some efforts were made to implement for alleviating the state explosion problem in the verification of concurrent
rect programs. The researches in formal methods emphasize on session type systems by embedding them to existing languag- programs. Instead of exploring global states, the compositional technique In order to help developers
the algorithmic, computational, practical aspects in the analy- es. Those implemented, however, are still far behind those ex- synthesizes local properties and verifies these properties on design compo-
sis of realistic programs. We apply mathematical and formal isting on paper, due to inexpressiveness of the type system in nents. In addition to classical finite concurrent programs, local reasoning has exploit the computational
techniques in the investigation of our research problems. We the host language. We plan to embed session type into Agda, been used to analyze parametric systems as well.
also aim to develop tools and methodologies to help develop- a language with an expressive dependent type system, hoping Local property synthesis is the key to the success of local reasoning. Tradi- power in parallel processors,
ers writing correct codes. to build an integrated environment in which programmers may tionally, local properties are obtained by fixed point computation. The itera-
program in Agda/Haskell, and use the type system to guaran- we are working on language
Multi-core processors are now widely used in desktop comput- tive computation however can be unnecessarily expensive. We plan to apply
ers, notebooks, and even smart- tee correctness and termination. algorithmic learning to the synthesis problem in local reasoning. When there and verification techniques
phones. Developers certainly We also plan to investigate the are lots of feasible local properties, algorithmic learning allows to infer one
would like to exploit concurrency “proofs-as-programs” approach to of them efficiently. Learning-based synthesis algorithms moreover give us for concurrent programs.
to improve the efficiency of appli- program correctness as embodied in more flexibility in the forms of inferred properties. Such flexibility will help us
cations. Yet concurrent program- proof assistants such as Coq and their understand local properties about programs.
ming is known to be difficult. program extraction mechanisms,
Even experienced developers may and to familiarize ourselves with the For average developers, applying formal techniques may be impractical due
make mistakes in writing concur- details of these tools so as to under- to the lack of training. Yet more and more concurrent programs are being
rent programs. Subsequently, stand their capacities and limitations. written by average developers. Verification tools for concurrent programs
there are still a very limited num- We have selected three application will undoubtedly help such developers improve their productivity. A large
ber of concurrent programs de- domains to work on: 1) Derivatives portions of existing concurrent programs are written by modern program-
spite of the prevalence of concur- of regular expressions, 2) Transforma- ming languages such as C++ and JAVA. For those existing codes, we also plan
rent computer systems. In order tions of structural contents, and 3) to develop automatic verification approaches that can ensure their correct-
to help developers exploit the Interactions of software components. ness. Precisely, we plan to develop concurrent software model checking ap-
computational power in modern The problems dealt with in the above proaches. The core technique of model checking is efficient exploration of
processors, the Programming three domains can often be related the entire state spaces of the program to be verified.
Languages and Formal Methods research group are currently to those encountered in general application development. For For concurrent program, the state space has to be explored is normally ex-
working on language and verification techniques for concur- example, Web application scripts shall process all user inputs tremely large due to the interleaving of behaviors of each individual thread.
rent programs. correctly (and avoiding common security pitfalls e.g. those In order to efficiently explore the state space, the use of abstraction tech-
caused by SQL Injection) and shall always produce correct out- nique is a must. We plan to combine existing abstraction techniques for con-
Type systems are widely deployed in modern programming puts (such as generating only valid XML documents). These is-
languages to ensure type safety. For example an ill-typed ex- sues fall into domains 1 and 2 above. How these scripts interact current programs. For example, we might use thread modular abstraction for
pression may add the number 0 to a character ‘0’ and evaluate with one another is also a major research issue (domain 3). We the control part and predicate abstraction for data part. The goal is scale up
to an incorrect result. Type systems allow developers to identify want to certify, by formal proofs, that the scripts for these ap- concurrent software model checking approach to programs that cannot be
such type errors at the compile time. Concurrent programming plications will have the required behaviors before they are de- handled by existing approaches.
is known to be error-prone, and the challenge of programmers ployed. These application domains will provide many interest- In addition to our research activities, we also dedicate significant resources
is even made harder when a modern program often consists ing and important problems for our investigation in program to education. In order to introduce our researches to students, we have or-
of hundreds or even thousands of threads communicating to constructions with formal proofs. ganized the yearly Formosan Summer School on Logic, Language, and Com-
each other. Modern programming languages adopt expressive putation (FLOLAC) since 2007. Through FLOLAC, more and more students in
type systems to guarantee certain properties of programs. Model checking is a technique to identify errors in program de- Taiwan have been encouraged to study and conduct research in program-
signs. Given an intended property about the design, a model ming languages and formal methods.
checker verifies the given property conclusively by exploring

研究群
36 Research Laboratories
36
37
37