Java Definite Assignment in Isabelle/HOL - CORE CORE Services Services overviewExplore all CORE services Access to raw data API Dataset FastSync Content discovery Recommender Discovery Managing content Repository dashboard Packages Repository edition About About us Our mission Team Blog FAQs Contact us research Java Definite Assignment in Isabelle/HOL Authors Norbert Schirmer Technische Universität München Publication date 2003 Publisher Abstract In Java the compiler guarantees that each local variable is initialised when we attempt to access it at runtime. This prohibits access to uninitialised memory during execution and is a key ingredient for type safety. We have formalised the definite assignment analysis of the Java compiler in the theorem prover Isabelle/HOL and proved it correct text Similar works Full text CiteSeerXProvided a free PDF (195.62 KB) View original full text link This paper was published in CiteSeerX. Having an issue? Is data on this page outdated, violates copyrights or anything else? Report the problem now and we will take corresponding actions after reviewing your request. Report Useful links Blog About CORE Contacts Cookies Privacy notice Accessibility Writing about CORE? Discover our research outputs and cite our work. CORE is a not-for-profit service delivered by The Open University and Jisc.
