We propose a new method to verify that a higher-order, tree-processing functional program conforms to an input/output specification. Our method reduces the verification problem to multiple verification problems for higher-order multi-tree transducers, which are then transformed into higher-order recursion schemes and model-checked. Unlike previous methods, our new method can deal with arbitrary higher-order functional programs manipulating algebraic data structures, as long as certain invariants on intermediate data structures are provided by a programmer. We have proved the soundness of the method and implemented a prototype verifier.

We introduce higher-order, multi-parameter, tree transducers (HMTTs, for short), which are kinds of higher-order tree transducers that take input trees and output a (possibly infinite) tree. We study the problem of checking whether the tree generated by a given HMTT conforms to a given output specification, provided that the input trees conform to input specifications (where both input/output specifications are regular tree languages). HMTTs subsume higher-order recursion schemes and ordinary tree transducers, so that their verification has a number of potential applications to verification of functional programs using recursive data structures, including resource usage verification, string analysis, and exact type-checking of XML-processing programs.

The JavaTM2 runtime system has a security mechanism which guarantees the code under execution has appropriate access permissions to a certain system resource. Use of this security mechanism requires access control policies to specify what operations are permitted on each such resource at each program point. Previous work proposed a program analysis algorithm to statically infer a semi-optimal policy set from given program text. However the proposed method cannot calculate the optimal policy when the target resource is determined by string values at run-time, since it does not keep track of all potential string values generated through built-in or user-defined methods. This results in generating excessive access policies where actually unnecessary resource accesses are permitted. To overcome such limitations, we apply static string analysis to program variables relevant to access control policies. This paper shows that unnecessary permissions can be reduced with string analysis by applying it to analyzing open-source libraries.

Recently Web browsers are widely used as client-side application platforms beyond the traditional use of Web browsers. One of main reasons for such evolution of the browsers is the client-side JavaScript language that can execute programs embedded in a document. However, Web applications with client-side JavaScript programs have problems of leaking private information (such as cookie information) due to interactions between the browser and scripts embedded in the document. We propose a new calculus representing browser behavior that prevents information from leakage by means of language-based information flow. The proposed calculus can deal with script rewriting and higher-order functions. In addition, our calculus has a noninterference property depending on a security policy statically given by the user.

We propose a new task scheduling algorithm for timed-functional simulation of concurrent software tasks. It attains efficiency by reducing the frequency of context-switching between concurrent tasks. It also provides a high-degree of portability in the sense that it only needs the underlying system to support a very small number of primitives. We provide a concrete implementation built on top of the SystemC scheduler and show some results of preliminary evaluation