TOP > Research > Department of Systems and Social Informatics > Department of Information Engineering > Software Science and Technology Group > NISHIDA, Naoki

Comprehensive List of Researchers "Information Knowledge"

Department of Information Engineering

Name
NISHIDA, Naoki
Group
Software Science and Technology Group
Title
Associate Professor
Degree
Dr. of Engineering
Research Field
Term rewriting system / Program transformation / Automated theorem proving
NISHIDA, Naoki

Current Research

Automatic Generation of Inverse Computation Programs in Functional Lauguages and its Application to Software Verification
Background -- what is inverse computation ?
The inverse computation of a program finds all possible input data of the program from the known output data of the program. Tools that generate inverse computation programs from given programs are called inversion compilers, and the given programs are called forward computation programs for the corresponding inverse computation programs. A practical instance of forward/inverse computation programs is zip/unzip programs. This instance tells us that forward/inverse computation programs must be reliable. Therefore, inversion compilers are useful for obtaining reliable forward/inverse computation programs if they automatically generate programs without bugs.

Outline of an Inversion Compiler
In our research, we try to construct an inversion compiler for term rewriting systems, one of the most typical computation models of functional languages.

The inversion compiler’s biggest advantage is that it generates programs without bugs. This is guaranteed by theoretically proving the correctness of the compiler. In the field of functional languages, many inversion compilers have been proposed without discussing correctness. Their correctness cannot be guaranteed even if their definitions seem intuitively correct. Such uncertainty of correctness is related to the evaluation order of forward computation. Up to now, it has remained unknown whether the inverse computation of forward computation not evaluated by “call-by-value” is possible. This problem was clarified in the process of constructing our compiler. Term rewriting systems are in simple form--their rules are pairs of terms. From this fact, we expect that proving the correctness of other inversion compilers can be reduced to the correctness proof of our approach.

When functions for forward computation are many-to-one, there may be some solutions for their inverse computation. Since term rewriting systems can express nondeterministic computation, there are computation paths to all solutions with respect to the programs generated by our compiler. In this case, by exhaustively searching all solutions, we can obtain all solutions. However, exhaustive searching is inefficient. In our research, we investigate reduction strategies for nondeterministic computation. One of our results is that innermost reduction effectively searches all solutions if programs have termination and a particular syntactic property.

Extension for Partial-Inverse Computation
We extend our inversion compiler for partial-inverse computation. The partial-inverse computation of a program is to find the remaining input data from the known output and some input of the program. For example, subtraction and division are partial-inverse computation operators of addition and multiplication, respectively. Moreover, encryption and decryption tools in the field of security protocols are partial-inverse programs. In those tools, common keys are used as known input. Partial-inverse computation is complicated but practical. Therefore, this research theme is interesting.

Future Works -- applications to software verification
Software verification is one application of inversion compilers. When an output and all input of a program are known, its partial-inverse computation program terminates if the input are valid for the known output. This performance verifies the relationship between output and input. Thus, this appears useful for verifying the program. Such an application of inversion compilers is one of our future works.
Figure : Overview of forward/inverse computations

Figure : Overview of forward/inverse computations

Career

  • Naoki Nishida received the Doctor of Engineering degree from Nagoya University in 2004.
  • He became a research associate of Nagoya University in April 2004.
  • He became an assistant professor of Nagoya University in April 2007.
  • He was a visiting researcher of DSIC at Technical University of Valencia from July to December in 2010.
  • He has been an associate professor of Nagoya University since April 2013.

Academic Societies

  • IEICE
  • JSSST
  • IPSJ

Publications

  1. Nishida, N., Sakai, M., and Sakabe, T., “Generation of Inverse Computation Programs of Constructor Term Rewriting Systems”, the IEICE Trans. on Inf. & Syst., Vol. J88-D-I, No. 8, pp. 1171-1183, 2005 (in Japanese).
  2. Nishida, N., Sakai, M., and Sakabe, T., “Computation Model of Term Rewriting Systems with Extra Variables”, Computer Software, Vol. 20, No. 5, pp. 85-89, 2003 (in Japanese).
  3. Nishida, N., Sakai, M., and Sakabe, T., “Generation of a TRS Implementing the Inverses of Pure Treeless Functions”, Computer Software, Vol. 19, No. 1, pp. 29-33, 2002 (in Japanese).
  4. Nishida, N., Sakai, M., and Sakabe,T., “Partial Inversion of Constructor Term Rewriting Systems", Proceedings of RTA 2005, LNCS 3467, pp. 264-278. 2005.
  5. Furuichi, Y., Nishida, N., Sakai, M., Kusakari, K., and Sakabe, T., “Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems”, IPSJ Transactions on Programming, Vol. 1, No. 2, pp. 100-121, 2008 (in Japanese).
  6. Sakata, T., Nishida, N., Sakabe, T., Sakai, M., and Kusakari, K., “Rewriting Induction for Constrained Term Rewriting Systems”, IPSJ Transactions on Programming, Vol. 2, No. 2, pp. 80-96, 2009 (in Japanese).
  7. Nishida, N. and Vidal, G., “Termination of Narrowing via Termination of Rewriting “, Applicable Algebra in Engineering, Communication and Computing, Vol. 21, No. 3, pp. 177-225, 2010.
  8. Nishida, N., Sakai, M., and Sakabe, T., "Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity", In Proc. of RTA 2011, Vol. 10 of LIPIcs, pp. 267-282, 2011.
  9. Nishida, N. and Vidal, G., "Program Inversion for Tail Recursive Functions", In Proc. of RTA 2011, Vol. 10 of LIPIcs, pp. 283-298, 2011.
  10. Sakata, T., Nishida, N., and Sakabe, T., "On Proving Termination of Constrained Term Rewriting Systems by Eliminating Edges from Dependency Graphs", In Proc. of WFLP 2011, Vol. 6816 of LNCS, pp. 138-155, 2011.
  11. Nishida , N. and Vidal, G., "More Specific Term Rewriting Systems", In Proc. of WFLP 2012, 15 pages, 2012.
  12. Nishida, N., Nomura, F., Kurahashi, K., and Sakai, M.. "Constrained Tree Automata and their Closure Properties", In Proc. of TTATT 2012, pp. 24-34, 2012.
  13. Nishida, N. and Vidal, G., "Computing More Specific Versions of Conditional Rewriting Systems", In Proc. of LOPSTR 2012, pp. 115-129, 2012.
  14. Niwa, M., Nishida, N., and Sakai, M., "Extending Matching Operation in Grammar Program for Program Inversion", In Proc of LOPSTR 2012, pp. 130-139, 2012.
  15. Nishida, N., Sakai, M., and Sakabe, T., "Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity", LMCS, Vol. 8, No. 3, pp. 1-49, 2012.
  16. Nishida, N. and Vidal, G., "Conversion to tail recursion in term rewriting," The Journal of Logic and Algebraic Programming, Vol. 83, Issu 1, pp. 53-63, Jan 2014.

BACK

top