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

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第1期190卷 19-33页

作者： Balland, Emilie Moreau, Pierre-Etienne Reilles, Antoine INRIA & LORIA LORIA F-54506 Vandoeuvre Les Nancy France INPL & LORIA LORIA F-54506 Vandoeuvre Les Nancy France

In this paper, we present a term rewriting based library for manipulating java bytecode. We define a mapping from bytecode programs to algebraic terms, and we use Tom, an extension of java that adds pattern-matching facilities, to describe transformations. An originality of Tom is that it provides a powerful strategy language to express traversals over trees and to control how transformation rules are applied. To be even more expressive, we use CTL formulae as conditions and we show how their satisfiability can be ensured using the strategy formalism. Through small examples, we show how bytecode analysis and transformations can be defined in an elegant way. In particular, we outline the implementation of a ClassLoader parameterized by a security policy that restricts file access.

关键词： Term rewriting java bytecode Tom CTL

来源：评论

学校读者我要写书评

暂无评论

Formal Translation of bytecode into BoogiePL

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第1期190卷 35-50页

作者： Lehner, Hermann Mueller, Peter Swiss Fed Inst Technol Zurich Switzerland

Many modern program verifiers translate the program to be verified and its specification into a simple intermediate representation and then compute verification conditions on this representation. Using an intermediate language improves the interoperability of tools and facilitates the computation of small verification conditions. Even though the translation into an intermediate representation is critical for the soundness of a verifier, this step has not been formally verified. In this paper, we formalize the translation of a small subset of java bytecode into an imperative intermediate language similar to BoogiePL. We prove soundness of the translation by showing that each bytecode method whose BoogiePL translation can be verified, can also be verified in a logic that operates directly on bytecode.

关键词： Program verification verification conditions intermediate language java bytecode BoogiePL

来源：评论

学校读者我要写书评

暂无评论

A Program Logic for bytecode

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2005年第1期141卷 255-273页

作者： Bannwart, Fabian Mueller, Peter ETH CH-8092 Zurich Switzerland

Program logics for bytecode languages such as java bytecode or the .NET CIL can be used to apply Proof-Carrying Code concepts to bytecode programs and to verify correctness properties of bytecode programs. This paper presents a Hoare-style logic for a sequential bytecode kernel language similar to java bytecode and CIL. The logic handles object-oriented features such as inheritance, dynamic method binding, and object structures with destructive updates, as well as unstructured control flow with jumps. It is sound and complete.

关键词： java bytecode .NET CIL program verification Hoare logic

来源：评论

学校读者我要写书评

暂无评论

Zpětný překladač bajtkódu jazyka java

Zpětný překladač bajtkódu jazyka Java

引用

作者： Hřibal, Jaromír Brno University of Technology

První část této bakalářské práce se zabývá základními principy virtuálního stroje jazyka java a detailněji se věnuje jeho instrukční sadě a formá... 详细信息

První část této bakalářské práce se zabývá základními principy virtuálního stroje jazyka java a detailněji se věnuje jeho instrukční sadě a formátu . class souborů, dohromady známých jako bajtkód . Následující část prezentuje rešerši existujících nástrojů pro manipulaci s bajtkódem . Poslední část popisuje vytvoření pluginu do vývojového prostředí Eclipse , který realizuje uživatelsky přívětivé zobrazení zadaného bajtkódu spolu s původním zdrojovým kódem, ze kterého byl bajtkód generován. Nástroj předpokládá dostupnost těchto zdrojových kódů, takže neplní roli dekompilátoru.

关键词： java Zpětný překlad java bajtkód java virtuální stroj java Disassembler java bytecode java Virtual Machine Text

来源：评论

学校读者我要写书评

暂无评论

Translate One, Analyze Many: Leveraging the Microsoft Intermediate Language and Source Code Transformation for Model Checking

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第1期190卷 3-18页

作者： McGeachie, Jesse Dingel, Juergen Queens Univ Sch Comp Kingston ON Canada

In this paper we present a source transformation-based framework to support model checking of source code written with languages belonging to Microsoft's. NET platform. The framework includes a set of source transformation rules to guide the transformation, tools to support assertion checking, as well as a tool for the automation of deadlock detection. The framework results in both executable and formally verifiable artifacts. We provide details of the tools in the framework, and evaluate the framework on a few small case studies.

关键词： Source transformation model checking TXL Microsoft Intermediate Language java bytecode

来源：评论

学校读者我要写书评

暂无评论

Encoding the java Virtual Machine's Instruction Set

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2010年第4期264卷 35-50页

作者： Eichberg, Michael Sewe, Andreas Tech Univ Darmstadt Dept Comp Sci Darmstadt Germany

New toolkits that parse, analyze, and transform java bytecode are frequently developed from scratch to obtain a representation suitable for a particular purpose. But, while the functionality implemented by these toolkits to read in class files and do basic control-and data-flow analyses is comparable, it is implemented over and over again. Differences manifest themselves mainly in minor technical issues. To avoid the repetitive development of similar functionality, we have developed an XML-based language for specifying bytecode- based instruction sets. Using this language, we have encoded the instruction set of the java Virtual Machine such that it can directly be used, e.g., to generate the skeleton of bytecode- based tools. The XML format hereby specifies both the format of the instructions and their effect on the stack and the local registers upon execution. This enables developers of static analyses to generate generic control-and data-flow analyses, e.g.,an analysis that transforms java bytecode into static single assignment form. To assess the usefulness of our approach, we have used the encoding of the java Virtual Machine's instruction set to develop a framework for the analysis and transformation of java class files. The evaluation shows that using the specification significantly reduces the development effort when compared to manual development.

关键词： java bytecode java Virtual Machine Specification XML

来源：评论

学校读者我要写书评

暂无评论

Capturing Program Models with BISM 22

Capturing Program Models with BISM

引用

37th Annual ACM Symposium on Applied Computing

作者： Soueidi, Chukri Falcone, Ylies Univ Grenoble Alpes INRIA CNRS Grenoble INPLIG Grenoble Grenoble France

ISBN: (纸本)9781450387132

In this paper, we present an extension of the java bytecode instrumentation tool BISM that captures and prepares a model that abstracts the program behavior at the intra-procedural level. We analyze program methods we are interested in monitoring and construct a control-flow graph automaton where the states represent actions of the program that produce events. Directed towards monitoring general behavioral properties at runtime, the resulting model is presented for the users to write static analyzers and combine both static and runtime verification.

关键词： Runtime Verification Typestate Analysis Parametric Monitoring Instrumentation java bytecode Control Flow

来源：评论

学校读者我要写书评

暂无评论

StoneDetector: Structural and Sub-Clone Detection 17

StoneDetector: Structural and Sub-Clone Detection

引用

IEEE 17th International Workshop on Software Clones (IWSC)

作者： Schaefer, Andre Amme, Wolfram Heinze, Thomas S. Friedrich Schiller Univ Jena Jena Germany Cooperat Univ Gera Eisenach Gera Germany

ISBN: (纸本)9798350344424

The StoneDetector system is an analysis system for finding code clones in java programs using control flow information. In contrast to well-known clone detectors, the StoneDetector system uses a special kind of control flow representation for code analysis, i.e., dominator trees. In previous work, the StoneDetector system has been shown to achieve better results for clone detection when compared to other text-based techniques, especially in case of structural code clones and subclones, as well as for code clones with larger syntactic variance. In this paper, after a brief introduction of the basic clone detection technique underlying the StoneDetector system, we present its architecture and its various operation modes working on java source code and bytecode.

关键词： clone detection dominator tree java bytecode java sourcecode

来源：评论

学校读者我要写书评

暂无评论

Parametric Inference of Memory Requirements for Garbage Collected Languages 10

Parametric Inference of Memory Requirements for Garbage Coll...

引用

2010 International Symposium on Memory Management

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

ISBN: (纸本)9781450300544

The accurate prediction of program's memory requirements is a critical component in software development. Existing heap space analyses either do not take deallocation into account or adopt specific models of garbage collectors which do not necessarily correspond to the actual memory usage. We present a novel approach to inferring upper bounds on memory requirements of java-like programs which is parametric on the notion of object lifetime, i.e., on when objects become collectible. If objects lifetimes are inferred by a reachability analysis, then our analysis infers accurate upper bounds on the memory consumption for a reachability-based garbage collector. Interestingly, if objects lifetimes are inferred by a heap liveness analysis, then we approximate the program minimal memory requirement, i.e., the peak memory usage when using an optimal garbage collector which frees objects as soon as they become dead. The key idea is to integrate information on objects lifetimes into the process of generating the recurrence equations which capture the memory usage at the different program states. If the heap size limit is set to the memory requirement inferred by our analysis, it is ensured that execution will not exceed the memory limit with the only assumption that garbage collection works when the limit is reached. Experiments on java bytecode programs provide evidence of the feasibility and accuracy of our analysis.

关键词： Languages Theory Verification Reliability Live Heap Space Analysis Peak Memory Consumption Low-level Languages java bytecode Garbage Collection

来源：评论

学校读者我要写书评

暂无评论

Live Heap Space Analysis for Languages with Garbage Collection 09

Live Heap Space Analysis for Languages with Garbage Collecti...

引用

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：