Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
421588 | Electronic Notes in Theoretical Computer Science | 2011 | 14 Pages |
Abstract
In this paper we describe a static analyser for Java bytecode which uses a combination of amortised analysis and Separation Logic due to Robert Atkey. With the help of Java annotations we are able to give precise resource utilisation constraints for Java methods which manipulate various heap-based data structures.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics