Sammapun, UsaSharykin, RamanDeLap, MargaretKim, MyongZdancewic, Stephan A2023-05-222023-05-222003-07-132005-08-23https://repository.upenn.edu/handle/20.500.14332/6175The Java-MaC framework is a run-time verification system for Java programs that can be used to dynamically test and enforce safety policies. This paper presents a formal model of the Java-MaC safety properties in terms of an operational semantics for Middleweight Java, a realistic subset of full Java. This model is intended to be used as a framework for studying the correctness of Java-MaC program instrumentation, optimizations, and future experimentation with run-time monitor expressiveness. As a preliminary demonstration of this model's applicability for these tasks, the paper sketches a correctness result for a simple program instrumentation scheme.Runtime verificationverificationPresentation