Loading...
Please wait, while we are loading the content...
Similar Documents
Taking into account Java ’ s Security Manager for static verification
| Content Provider | Semantic Scholar |
|---|---|
| Author | Charles, Julien |
| Copyright Year | 2007 |
| Abstract | The verification of Java programs is a difficult task, especially with components like the Security Manager which modify the semantic of the Java Virtual Machine (JVM). To model this invasive behaviour the Security Manager can be implemented as an aspect component, using AspectJ. In this paper we describe a framework for static verification of Java programs containing AspectJ advices specified with Pipa and we instanciate it over a case study, the Security Manager. The framework is built around a weakest precondition calculus over Java bytecode using guarded commands. It has an advice weaving semantic which is correct against AspectJ advice weaving semantic. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www-sop.inria.fr/everest/personnel/Julien.Charles/papers/07-08-10-aspects.pdf |
| Alternate Webpage(s) | https://www-sop.inria.fr/everest/Julien.Charles/papers/07-08-10-aspects.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |