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