Generating Java Compiler Optimizers Using Bidirectional CTL

There have been several research works that analyze and optimize programs using temporal logic. However, no evaluation of optimization time or execution time of these implementations has been done for any real programming language. In this paper, we present a system that generates a Java optimizer from specifications in temporal logic. The specification is simpler, and the generated optimizers run more efficiently than previously reported work. We implemented a new model checker for a bidirectional CTL (computational tree logic) called CTLbd, which is equivalent to CTL-FV [9] after removing free variables. The model checker can check future and past temporal CTL operators symmetrically without any conversion. We also present a new specification language based on the bidirectional CTL that can express typical optimization rules very naturally. By adding rewriting conditions to allow for temporary variables and considering real-world language features such as exceptions, the system c...

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Ling Fang, Masataka Sassa
• Keywords: Bidirectional Ctl, ENTCS 2007, Real Programming Language, Temporal Logic