ComplexityParser: An Automatic Tool for Certifying Poly-Time Complexity of Java Programs

Emmanuel Hainry (1) , Emmanuel Jeandel (1) , Romain Péchoux (1) , Olivier Zeyen (1)

1 MOCQUA - Designing the Future of Computational Models

ComplexityParser is a static complexity analyzer for Java programs providing the first implementation of a tier-based typing discipline. The input is a file containing Java classes. If the main method can be typed and, provided the program terminates, then the program is guaranteed to do so in polynomial time and hence also to have heap and stack sizes polynomially bounded. The application uses antlr to generate a parse tree on which it performs an efficient type inference: linear in the input size, provided that the method arity is bounded by some constant.

Domaines: Complexité [cs.CC]; Langage de programmation [cs.PL]

Emmanuel Hainry, Emmanuel Jeandel, Romain Péchoux, Olivier Zeyen. ComplexityParser: An Automatic Tool for Certifying Poly-Time Complexity of Java Programs. ICTAC 2021 - 18th International Colloquium on Theoretical Aspects of Computing, Sep 2021, Nur-Sultan/Virtual, Kazakhstan. pp.357-365, ⟨10.1007/978-3-030-85315-0_20⟩. ⟨hal-03337755⟩