检索结果-内蒙古大学图书馆

International Conference on Memory Management

作者： Albert, Elvira Genaim, Samir Gomez-Zamalloa, Miguel Univ Complutense Madrid E-28040 Madrid Spain

ISBN: (纸本)9781605583471

The peak heap consumption of a program is the maximum size of the live data on the heap during the execution of the program, i.e., the minimum amount of heap space needed to run the program without exhausting the memory. It is well-known that garbage collection (GC) makes the problern of predicting the memory required to run a program difficult. This paper presents, the best of our knowledge, the first live heap space analysis for garbage-collected languages which infers accurate upper bounds on the peak heap usage of a program's execution that are not restricted to any complexity class, i.e., we can infer exponential, logarithmic, polynomial, etc., bounds. Our analysis is developed for an (sequential) object-oriented bytecode language with a scoped-memory manager that reclaims unreachable memory when methods return. We also show how our analysis can accommodate other GC schemes which are closer to the ideal GC which collects objects as soon as they become unreachable. The practicality of our approach is experimentally evaluated on a prototype implementation. We demonstrate that it is fully automatic, reasonably accurate and efficient by inferring live heap space bounds for a standardized set of benchmarks, the JOlden suite.

关键词： Live Heap Space Analysis Peak Memory Consumption Low-level Languages java bytecode

来源：评论

学校读者我要写书评

暂无评论

An approach for analyzing bytecode information flow

An approach for analyzing bytecode information flow

引用

International Symposium on Communications and Information Technologies (ISCIT2005)

作者： Bian, GW Nakayama, K Kobayashi, Y Maekawa, M Univ Electrocommun Dept Informat Syst Tokyo Japan

ISBN: (纸本)0780395387

Existing approaches are inadequate to address the information flow in java bytecode and the type systems verification often used in these approaches is imprecise. This paper presents a method to disclose java bytecode information flow, in which the information dependence relationship among the variables in the bytecode is determined by data-flow analysis and information flow policy is verified by type-checking method. Since the analysis object is bytecode, this approach can be used for java mobile code systems. The precision of verification can be improved because of this approach.

关键词： java bytecode dependence analysis information flow

来源：评论

学校读者我要写书评

暂无评论

BISM: bytecode-Level Instrumentation for Software Monitoring 20th

BISM: Bytecode-Level Instrumentation for Software Monitoring

引用

20th International Conference on Runtime Verification (RV)

作者： Soueidi, Chukri Kassem, Ali Falcone, Ylies Univ Grenoble Alpes INRIA CNRS Grenoble INPLIG F-38000 Grenoble France

ISBN: (纸本)9783030605087;9783030605070

BISM (bytecode-level Instrumentation for Software Monitoring) is a lightweight java bytecode instrumentation tool which features an expressive high-level control-flow-aware instrumentation language. The language follows the aspect-oriented programming paradigm by adopting the joinpoint model, advice inlining, and separate instrumentation mechanisms. BISM provides joinpoints ranging from bytecode instruction to method execution, access to comprehensive context information, and instrumentation methods. BISM runs in two modes: build-time and load-time. We demonstrate BISM effectiveness using two experiments: a security scenario and a general runtime verification case. The results show that BISM instrumentation incurs low runtime and memory overheads.

关键词： Instrumentation Runtime verification Monitoring java bytecode Aspect-oriented programming Control flow Static and dynamic contexts

来源：评论

学校读者我要写书评

暂无评论

javaPDG: A New Platform for Program Dependence Analysis

JavaPDG: A New Platform for Program Dependence Analysis

引用

6th IEEE International Conference on Software Testing, Verification and Validation (ICST)

作者： Shu, Gang Sun, Boya Henderson, Tim A. D. Podgurski, Andy Case Western Reserve Univ Dept Elect Engn & Comp Sci Cleveland OH 44106 USA

ISBN: (纸本)9780769549682

Dependence analysis is a fundamental technique for program understanding and is widely used in software testing and debugging. However, there are a limited number of analysis tools available despite a wide range of research work in this field. In this paper, we present javaPDG(1), a static analyzer for java bytecode, which is capable of producing various graphical representations such as the system dependence graph, procedure dependence graph, control flow graph and call graph. As a program-dependence-graph based analyzer, javaPDG performs both intra- and inter-procedural dependence analysis, and enables researchers to apply a wide range of program analysis techniques that rely on dependence analysis. javaPDG provides a graphical viewer to browse and analyze the various graphs and a convenient JSON based serialization format.

关键词： program dependence graph system dependence graph procedure dependence graph call graph java Virtual Machine java bytecode

来源：评论

学校读者我要写书评

暂无评论

Using a molecular metaphor to facilitate comprehension of 3D object diagrams

Using a molecular metaphor to facilitate comprehension of 3D...

引用

IEEE Symposium on Visual Languages and Human-Centric Computing

作者： Malloy, BA Power, JF Clemson Univ Clemson SC 29631 USA

ISBN: (纸本)0769524435

This paper presents a strategy for the visualization of dynamic object relationships in java programs. The metaphor of a chemical molecule is used to aid Comprehension, and to help in reducing the size of the object graph. Our strategy has been implemented by dynamically instrumenting java bytecode to collect trace data, which is then analyzed and visualized in 3D using VRML. Quantitative and graphical results are presented, based on an analysis of programs in the SPEC JVM98 and JOlden benchmark suites.

关键词： java data visualisation formal specification object-oriented programming program visualisation virtual reality languages 3D object diagrams JOlden java bytecode java programs SPEC JVM98 VRML chemical molecule dynamic object relationship visualization mol

来源：评论

学校读者我要写书评

暂无评论

Software watermarking through register allocation: Implementation, analysis, and attacks

引用

6th International Conference on Information Security and Cryptology

作者： Myles, G Collberg, C Univ Arizona Dept Comp Sci Tucson AZ 85721 USA

ISBN: (纸本)3540213767

In this paper we explore the application of the QP water-marking algorithm proposed by G. Qu and M. Potkonjak to software watermarking. The algorithm was originally proposed as a technique for watermarking the graph coloring problem which can be applied to a variety of media such as FPGA designs and software through register allocation. We implemented the algorithm within the SandMark framework, a system that allows the study of watermarking, tamper-proofing, and obfuscation algorithms for java bytecode. Through the use of this framework we were able to perform an empirical evaluation of the algorithm. In particular we demonstrate that the use of register allocation, while incurring no performance overhead and being stealthy, is in fact vulnerable to attacks such as decompile/recompile. We also demonstrate that the QP algorithm does not allow for accurate watermark recognition without, significant modifications.

关键词： copyright protection register allocation java bytecode software piracy software watermarking

来源：评论

学校读者我要写书评

暂无评论

Evolving Software Building Blocks with FINCH 17

Evolving Software Building Blocks with FINCH

引用

Genetic and Evolutionary Computation Conference (GECCO)

作者： Orlov, Michael Shamoon Coll Engn Beer Sheva Israel

This paper proposes to explore the following question: can software evolution systems like FINCH, that evolve linear representations originating from a higher-level structural language, take advantage of building bloc... 详细信息

ISBN: (纸本)9781450349390

关键词： Genetic improvement java bytecode genetic programming

来源：评论

学校读者我要写书评

暂无评论

A compositional account of the java virtual machine 99

A compositional account of the Java virtual machine

引用

Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

作者： Phillip M. Yelland Sun Microsystems Laboratories 910 San Antonio Road MS MTV29-117 Palo Alto CA

ISBN: (纸本)9781581130959

The java Virtual Machine (or JVM) is central to the system's aim of providing a secure program execution environment that operates identically on a wide variety of computing platforms. To be most effective in this role, the JVM needs a rigorous, complete description, to specify precisely the behavior required of implementations. In response, a number of researchers have produced formal accounts of the JVM that seek to define it in an unambiguous and comprehensible manner. Unfortunately, the size and complexity of the JVM means that many of these formal accounts must either restrict their scope substantially, or risk becoming unwieldy and intractable. This paper suggests an alternative approach to the specification of the JVM that seeks to ameliorate such problems by composing together a small set of "microinstructions" to produce the full bytecode set. These microinstructions are encapsulated as functions in the polymorphic functional programming language Haskell, using the familiar mechanisms of Hindley-Milner type inference to characterize the JVM's rather thorny verifier. In this way, its is hoped that a foundation will be laid for formal descriptions of the java Virtual Machine that need not trade tractability for completeness.

关键词： Haskell java bytecode java virtual machine verification

来源：评论

学校读者我要写书评

暂无评论

AMORTISED RESOURCE ANALYSIS WITH SEPARATION LOGIC

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2011年第2期7卷

作者： Atkey, Robert Univ Strathclyde Glasgow G1 1XQ Lanark Scotland

Type-based amortised resource analysis following Hofmann and Jost where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline-have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative pointer-manipulating languages by embedding a logic of resources, based on the affine intuitionistic Logic of Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the consumable resources associated with each member of the structure. We present the logic on a small imperative language, based on java bytecode, with procedures and mutable heap. We have formalised the logic and its soundness property within the Coq proof assistant and extracted a certified verification condition generator. We also describe an proof search procedure that allows generated verification conditions to be discharged while using linear programming to infer consumable resource annotations. We demonstrate the logic on some examples, including proving the termination of in-place list reversal on lists with cyclic tails.

关键词： resource bounded computing amortised analysis separation logic java bytecode program logic resource models

来源：评论

学校读者我要写书评

暂无评论

SECURE THE CLONES

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2012年第2期8卷 5-5页

作者： Jensen, Thomas Kirchner, Florent Pichardie, David INRIA Rennes Bretagne Atlantique Bretagne France

Exchanging mutable data objects with untrusted code is a delicate matter because of the risk of creating a data space that is accessible by an attacker. Consequently, secure programming guidelines for java stress the importance of using defensive copying before accepting or handing out references to an internal mutable object. However, implementation of a copy method (like clone()) is entirely left to the programmer. It may not provide a sufficiently deep copy of an object and is subject to overriding by a malicious sub-class. Currently no language-based mechanism supports secure object cloning. This paper proposes a type-based annotation system for defining modular copy policies for class-based object-oriented programs. A copy policy specifies the maximally allowed sharing between an object and its clone. We present a static enforcement mechanism that will guarantee that all classes fulfil their copy policy, even in the presence of overriding of copy methods, and establish the semantic correctness of the overall approach in Coq. The mechanism has been implemented and experimentally evaluated on clone methods from several java libraries.

关键词： Static analysis Shape analysis Type system java bytecode Secure data copying

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：