Page 39 - profile2014.indd

Injection) and shall always produce correct outputs (such as For concurrent program, the state space has to be explored is
generating only valid XML documents). These issues fall into normally extremely large due to the interleaving of behaviors
domains 1 and 2 above. How these scripts interact with one an- of each individual thread. In order to efficiently explore the
other is also a major research issue (domain 3). We want to cer- state space, the use of abstraction technique is a must. We plan
tify, by formal proofs, that the scripts for these applications will to combine existing abstraction techniques for concurrent pro-
have the required behaviors before they are deployed. These grams. For example, we might use thread modular abstraction
application domains will provide many interesting and impor- for the control part and predicate abstraction for data part. The
tant problems for our investigation in program constructions goal is scale up concurrent software model checking approach
with formal proofs. to programs that cannot be handled by existing approaches.

Model checking is a technique to identify errors in program de- In addition to our research activities, we also dedicate signifi-
signs. Given an intended property about the design, a model cant resources to education. In order to introduce our research-
checker verifies the given property conclusively by exploring es to students, we have organized the yearly Formosan Summer
all design behaviors. For concurrent systems, the number of School on Logic, Language, and Computation (FLOLAC) since
design behaviors grows exponentially in the number of design 2007. Through FLOLAC, more and more students in Taiwan have
components. This is the infamous state explosion problem. Lo- been encouraged to study and conduct research in program-
cal reasoning is a compositional technique for alleviating the ming languages and formal methods.
state explosion problem in the verification of concurrent pro-
grams. Instead of exploring global states, the compositional
technique synthesizes local properties and verifies these prop-
erties on design components. In addition to classical finite con-
current programs, local reasoning has been used to analyze
parametric systems as well.

Local property synthesis is the key to the success of local rea-
soning. 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 prop-
erties. 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 con-
current programs are being written by average developers.
Verification tools for concurrent programs will undoubtedly
help such developers improve their productivity. A large por-
tions of existing concurrent programs are written by modern
programming languages such as C++ and JAVA. For those ex-
isting codes, we also plan to develop automatic verification ap-
proaches 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.

39