A Java Supercompiler and Its Application to Verification of Cache-Coherence Protocols

Abstract. The Java Supercompiler (JScp) is a specializer of Java programs based on the Turchin's supercompilation method and extended to support imperative and object-oriented notions absent in functional languages. The results of successful application of the Java Supercompiler for verification of a number of parameterized models of cache-coherence protocols are reported. Protocols are modeled in Java following the known method by G. Delzanno and experiments by A. Lisitsa and A. Nemytykh on verification of protocol models by means of the Refal Supercompiler SCP4. The part of the supercompilation method relevant to the protocol verification is described. It deals with an imperative subset of Java.

• Type: Conference
• Year: 2009
• Where: ERSHOV
• Authors: Andrei V. Klimov
• Keywords: ERSHOV 2009, Java Supercompiler, Supercompilation Method, Theoretical Computer Science, Turchin's Supercompilation Method