Using CLP Simplifications to Improve Java Bytecode Termination Analysis

Fausto Spoto; Lunjin Lu; Frédéric Mesnard

Using CLP Simplifications to Improve Java Bytecode Termination Analysis

Fausto Spoto ¹ Lunjin Lu Frédéric Mesnard ^{2, 3}

2 IREMIA - Institut de REcherche en Mathématiques et Informatique Appliquées

3 LIM - Laboratoire d'Informatique et de Mathématiques

Abstract : In an earlier work, a termination analyzer for Java bytecode was developed that translates a Java bytecode program into a constraint logic program and then proves the termination of the latter. An efficiency bottleneck of the termination analyzer is the construction of a proof of termination for the generated constraint logic program, which is often very large in size. In this paper, a set of program simplifications are presented that reduce the size of the constraint logic program without changing its termination behavior. These simplifications remove program clauses and/or predicate arguments that do not affect the termination behavior of the constraint logic program. Their effect is to reduce significantly the time needed to build the termination proof for the constraint logic program, as our experiments show.

Keywords : Java Java bytecode static analysis termination

Document type :

Conference papers

Domain :

Computer Science [cs]

Complete list of metadatas

Cited literature [18 references] Display Hide Download

http://hal.univ-reunion.fr/hal-01188704
Contributor : Nicolas Alarcon <>
Submitted on : Thursday, June 7, 2018 - 7:27:12 AM
Last modification on : Thursday, March 28, 2019 - 11:24:11 AM
Long-term archiving on : Saturday, September 8, 2018 - 12:59:53 PM

1-s2.0-S1571066109004691-main....

Publication funded by an institution

Using CLP Simplifications to Improve Java Bytecode Termination Analysis

File

Identifiers

Collections

Citation

Export

Metrics

91

76

Contact

Using CLP Simplifications to Improve Java Bytecode Termination Analysis

File

Identifiers

Collections

Citation

Export

Share

Metrics

91

76

Contact