Complexity Analysis in Java using a Type System

Advisors

  • Romain Péchoux , LORIA, Université de Lorraine, Nancy, France
  • Emmanuel Hainry , LORIA, Université de Lorraine, Nancy, France

Domain

The aim of Implicit Complexity is to design criteria (type systems, semantic interpretations) to prove that programs belong to given classes of complexity. A new implicit complexity analysis based on a type system for imperative and object oriented languages was proposed in articles [1], [2] and [7]. This analysis is inspired by Data Ramification techniques [3, 4] and by non-interference [5]. It ensures that if a program can be typed and terminates, it will run in polynomial time (or in a different context, polynomial space).

Goal

The goal will be to extend the existing type system to capture more features of Object Oriented Programs, while still ensuring polynomial time or polynomial space execution.

This work should focus on the following ideas:

  • increase the number of programs that can be analysed through the use of program transformation techniques;
  • improve the expressivity of the considered language by considering forks, threads, functions, exceptions for example.
  • explore the common cases in real world programs for which this analysis fails and correct the type system to capture them.

Prerequisite

Knowledge of Java (or similar Object Oriented Language), good understanding of the theory of complexity and of type theory would be welcome.

References

  1. J.-Y. Marion, A Type System for Complexity Flow Analysis. LICS 2011, pp. 123-132 (2011)
  2. J.-Y. Marion, R. Péchoux, Complexity Information Flow in a Multi-threaded Imperative Language CoRR abs/1203.6878 (2012)
  3. S. Bellantoni and S. Cook, A new recursion-theoretic characterization of the poly-time functions, Computational Complexity 2 (1992), p. 97–110.
  4. D. Leivant and J.-Y. Marion, Lambda calculus characterizations of poly-time, Fundamenta Informaticae 19 (1993), no. 1,2, p. 167,184.
  5. Dennis M. Volpano, Cynthia E. Irvine, Geoffrey Smith, A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4(2/3): 167-188 (1996)
  6. Byron Cook, Andreas Podelski, Andrey Rybalchenko, Terminator: Beyond Safety. CAV 2006, 415-418
  7. E. Hainry, R. Péchoux, Type-based heap and stack space analysis in Java, http://hal.inria.fr/hal-00773141, 2013