Formalizing Java-MaC
Embargo Date
Related Collections
Degree type
Discipline
Subject
verification
Funder
Grant number
License
Copyright date
Distributor
Related resources
Contributor
Abstract
The 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.
Advisor
Date of presentation
Conference name
Conference dates
Conference location
Date Range for Data Collection (Start Date)
Date Range for Data Collection (End Date)
Digital Object Identifier
Series name and number
Volume number
Issue number
Publisher
Publisher DOI
Comments
Postprint version. Published in Electronic Notes in Theoretical Computer Science, Volume 89, Issue 2, October 2003, 20 pages. Publisher URL: http://dx.doi.org/10.1016/S1571-0661(04)81048-X