Flow Logic for Imperative Objects

We develop a control flow analysis for the Imperative Object Calculus. We prove the correctness with respect to two Structural Operational Semantics that differ in minor technical ways, and we show that the proofs deviate in major ways as regards their use of proof techniques like coinduction and Kripke-logical relations.

• Type: Conference
• Year: 1998
• Where: MFCS
• Authors: Flemming Nielson, Hanne Riis Nielson
• Keywords: Imperative Object Calculus, MFCS 1998, Minor Technical Ways, Structural Operational Semantics, Theoretical Computer Science