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

28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Held as Part of the 25th European Joint Conferences on Theory and Practice of Software (ETAPS)

作者： Wu, Tong Schrammel, Peter Cordeiro, Lucas C. Univ Manchester Manchester Lancs England Univ Sussex Brighton E Sussex England Diffblue Ltd Oxford England

ISBN: (纸本)9783030995270;9783030995263

We describe and evaluate a violation-witness validator for java verifiers called Wit4java. It takes a java program with a safety property and the respective violation-witness output by a java verifier to generate a new java program whose execution deterministically violates the property. We extract the value of the program variables from the counterexample represented by the violation-witness and feed this information back into the original program. In addition, we have two implementations for instantiating source programs by injecting counterexamples. Experimental results show that Wit4java can correctly validate the violation-witnesses produced by JBMC and GDart in a few seconds.

关键词： Witness Validation Software Verification java bytecode

来源：评论

学校读者我要写书评

暂无评论

Advanced POC model-based java instruction folding mechanism

Advanced POC model-based Java instruction folding mechanism

引用

26th Euromicro Conference

作者： Kim, A Chang, M IIT Dept Comp Sci Chicago IL 60616 USA

ISBN: (纸本)0769507808;0769507816

Ever since java was introduced world wide, the execution performance has always been a problem. As one of the solutions, a bytecode instruction folding process far java processors was developed in a Picojava model and a Producer, Operator and Consumer (POC) model, but if could not handle certain types of instruction sequences. In this paper, a new instruction folding scheme based on a new, advanced POC model is proposed and demonstrates improvement in bytecode execution. The proposed POC model is able to detect and fold all possible instruction sequence types dynamically in hardware, including a sequence that is separated by other bytecode instructions. SPEC JMV98 benchmark results shaw that the proposed POC model-based folder can save more than 90% of folding operations. In addition, a design of the proposed POC model-based folding process in hardware is much smaller and more efficient than traditional folding mechanisms.

关键词： instruction folding stack java programming language java bytecode java processor java Virtual Machine (JVM)

来源：评论

学校读者我要写书评

暂无评论

Precise null-pointer analysis

引用

SOFTWARE AND SYSTEMS MODELING 2011年第2期10卷 219-252页

作者： Spoto, Fausto Univ Verona I-37100 Verona Italy

In java, C or C++, attempts to dereference the null value result in an exception or a segmentation fault. Hence, it is important to identify those program points where this undesired behaviour might occur or prove the other program points (and possibly the entire program) safe. To that purpose, null-pointer analysis of computer programs checks or infers non-null annotations for variables and object fields. With few notable exceptions, null-pointer analyses currently use run-time checks or are incorrect or only verify manually provided annotations. In this paper, we use abstract interpretation to build and prove correct a first, flow and context-sensitive static null-pointer analysis for java bytecode (and hence java) which infers non-null annotations. It is based on Boolean formulas, implemented with binary decision diagrams. For better precision, it identifies instance or static fields that remain always non-null after being initialised. Our experiments show this analysis faster and more precise than the correct null-pointer analysis by Hubert, Jensen and Pichardie. Moreover, our analysis deals with exceptions, which is not the case of most others;its formulation is theoretically clean and its implementation strong and scalable. We subsequently improve that analysis by using local reasoning about fields that are not always non-null, but happen to hold a non-null value when they are accessed. This is a frequent situation, since programmers typically check a field for non-nullness before its access. We conclude with an example of use of our analyses to infer null-pointer annotations which are more precise than those that other inference tools can achieve.

关键词： Null-pointer analysis java bytecode Static analysis Abstract interpretation Automatic software verification

来源：评论

学校读者我要写书评

暂无评论

LibCapsule: Complete Confinement of Third-Party Libraries in Android Applications

引用

IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING 2022年第5期19卷 2873-2889页

作者： Qiu, Jun Yang, Xuewu Wu, Huamao Zhou, Yajin Li, Jinku Ma, Jianfeng Xidian Univ Sch Cyber Engn Xian 710071 Shaanxi Peoples R China Zhejiang Univ Coll Comp Sci & Technol Sch Cyber Space & Technol Hangzhou 310027 Zhejiang Peoples R China

Android application (or app) developers increasingly integrate third-party libraries to enrich the functionality of their apps. However, current permission model on Android cannot constrain the behaviors of in-app third-party libraries for allowing them to operate with the same permissions as their host app. This brings serious security and privacy concerns to users. In this article, we propose LibCapsule, a user-level solution to confine third-party libraries from potential permission abuses. Compared to previous systems, LibCapsule is able to provide complete confinement of third-party libraries in Android apps, including the static java code, dynamically loaded code and native code of third-party libraries. We have developed a prototype of LibCapsule, and collected 204 popular third-party libraries as well as 2,021 apps to evaluate it. The evaluation results indicate that LibCapsule is capable of enforcing complete and fine-grained regulation on third-party libraries according to customized security policies with a low performance overhead. To engage the whole community, we will release the dataset of third-party libraries and apps in our evaluation.

关键词： Libraries Security java Smart phones Runtime Privacy Servers Third-party library java bytecode dynamically loaded code native code

来源：评论

学校读者我要写书评

暂无评论

Verifying pointer programs using graph grammars

引用

SCIENCE OF COMPUTER PROGRAMMING 2015年第Part1期97卷 157-162页

作者： Heinen, Jonathan Jansen, Christina Katoen, Joost-Pieter Noll, Thomas Rhein Westfal TH Aachen Software Modeling & Verificat Grp Aachen Germany

This paper argues that graph grammars naturally model dynamic data structures such as lists, trees and combinations thereof. These grammars can be exploited to obtain finite abstractions of pointer-manipulating programs, thus enabling model checking. Experimental results for verifying Lindstrom's variant of the Deutsch-Schorr-Waite tree traversal algorithm illustrate this. (C) 2013 Elsevier B.V. All rights reserved.

关键词： Hyperedge replacement grammars java bytecode Dynamic data structures Verification

来源：评论

学校读者我要写书评

暂无评论

SeByte: Scalable clone and similarity search for bytecode

引用

SCIENCE OF COMPUTER PROGRAMMING 2014年第Part4期95卷 426-444页

作者： Keivanloo, Iman Roy, Chanchal K. Rilling, Juergen Queens Univ Dept Elect & Comp Engn Kingston ON K7L 3N6 Canada Univ Saskatchewan Dept Comp Sci Saskatoon SK S7N 0W0 Canada Concordia Univ Dept Comp Sci Montreal PQ Canada

While source code clone detection is a well-established research area, finding similar code fragments in binary and other intermediate code representations has been not yet that widely studied. In this paper, we introduce SeByte, a bytecode clone detection and search model that applies semantic-enabled token matching. It is developed based on the idea of relaxation on the code fingerprints. This approach separates the input content based on the types of tokens into different dimensions, with each dimension representing the input content from a specific point of view. Following this approach, SeByte compares each dimension separately and independently which we refer to as multi-dimensional comparison in our research. As the similarity search function we use a well-known measure that supports our multi-dimensional comparison heuristic, the Jaccard similarity coefficient. Our preliminary study shows that SeByte can detect clones that are missed by existing approaches due to the differences in the input data and the search algorithm. We then further exploit the model to build a scalable bytecode clone search engine. This extension meets the requirements of a classical search engine including the ranking of result sets. Our evaluation with a large dataset of 500,000 compiled java classes, which we extracted from the six most recent versions of the Eclipse IDE, showed that our SeByte search is not only scalable but also capable of providing a reliable ranking. (C) 2013 Elsevier B.V. All rights reserved.

关键词： Clone detection Semantic Web java bytecode Clone search Semantic search

来源：评论

学校读者我要写书评

暂无评论

Heap space analysis for garbage collected languages

引用

SCIENCE OF COMPUTER PROGRAMMING 2013年第9期78卷 1427-1448页

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

Accurately predicting the dynamic memory consumption (or heap space) of programs can be critical during software development. It is well-known that garbage collection (GC) complicates such problem. The peak heap consumption of a program is the maximum size of the data on the heap during its execution, i.e., the minimum amount of heap space needed to safely run the program. 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. This paper presents a novel static analysis for garbage-collected imperative languages that infers accurate upper bounds on the peak heap usage, including exponential, logarithmic and polynomial bounds. A unique characteristic of the analysis is that it is parametric on the notion of object lifetime, i.e., on when objects become collectible. (C) 2012 Elsevier B.V. All rights reserved.

关键词： Static analysis Live heap space analysis Peak memory consumption Low-level languages java bytecode Garbage collection

来源：评论

学校读者我要写书评

暂无评论

Conditional termination of loops over heap-allocated data

引用

SCIENCE OF COMPUTER PROGRAMMING 2014年第PartA期92卷 2-24页

作者： Alberta, Elvira Arenas, Puri Genaim, Samir Puebla, German Roman-Diez, Guillermo Complutense Univ Madrid UCM DSIC Madrid Spain Tech Univ Madrid UPM DLSIIS Madrid Spain

Static analysis which takes into account the values of data stored in the heap is considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields nor of array contents, i.e., they are heap-insensitive. In this article, we propose locality conditions for soundly tracking heap-allocated data in java (bytecode) programs, by means of ghost non-heap allocated variables. This way, heap-insensitive analysis over the transformed program can infer information on the original heap-allocated data without sacrificing efficiency. If the locality conditions cannot be proven unconditionally, we seek to generate aliasing preconditions which, when they hold in the initial state, guarantee the termination of the program. Experimental results show that we greatly improve the accuracy w.r.t. a heap-insensitive analysis while the overhead introduced is reasonable. (C) 2013 Elsevier B.V. All rights reserved.

关键词： Static analysis Heap-sensitive analysis Termination java bytecode Program transformation

来源：评论

学校读者我要写书评

暂无评论

ARDEN2bytecode: A one-pass Arden Syntax compiler for service-oriented decision support systems based on the OSGi platform

引用

COMPUTER METHODS AND PROGRAMS IN BIOMEDICINE 2012年第2期106卷 114-125页

作者： Gietzelt, Matthias Goltz, Ursula Grunwald, Daniel Lochau, Matte Marschollek, Michael Song, Bianying Wolf, Klaus-Hendrik Tech Univ Carolo Wilhelmina Braunschweig Inst Technol Peter L Reichertz Inst Med Informat D-38106 Braunschweig Germany Hannover Med Sch D-38106 Braunschweig Germany Tech Univ Carolo Wilhelmina Braunschweig Inst Technol Inst Programming & React Syst D-38106 Braunschweig Germany

Patient empowerment might be one key to reduce the pressure on health care systems challenged by the expected demographic changes. Knowledge based systems can, in combination with automated sensor measurements, improve the patients' ability to review their state of health and make informed decisions. The Arden Syntax as a standardized language to represent medical knowledge can be used to express the corresponding decision rules. In this paper we introduce ARDEN2bytecode, a newly developed open source compiler for the Arden Syntax. ARDEN2bytecode runs on java Virtual Machines (JVM) and translates Arden Syntax directly to java bytecode (JBC) executable on JVMs. ARDEN2bytecode easily integrates into service oriented architectures, like the Open Services Gateway Initiative (OSGi) platform. Apart from an evaluation of compilation performance and execution times, ARDEN2bytecode was integrated into an existing knowledge supported exercise training system and recorded training sessions have been used to check the implementation. (c) 2011 Elsevier Ireland Ltd. All rights reserved.

关键词： Arden Syntax java bytecode Decision support Knowledge based systems Compiler Service oriented architecture

来源：评论

学校读者我要写书评

暂无评论

Extrakce grafu toku řízení z bajtkódu java

Extrakce grafu toku řízení z bajtkódu Java

引用

作者： Sečkařová, Petra Brno University of Technology

Grafy toku řízení (Control Flow Graph -- CFG) slouží jako základ pro mnoho analýz vyhodnocujících kvalitu programu. Takovou analýzou je i testování založené na mo... 详细信息

Grafy toku řízení (Control Flow Graph -- CFG) slouží jako základ pro mnoho analýz vyhodnocujících kvalitu programu. Takovou analýzou je i testování založené na modelech (model-based testing), které na základě analýzy modelu kódu, např. grafu, generuje testovací případy. Aby bylo možné tuto analýzu provádět co nejobecněji, je vhodné, aby instrukce obsažené v CFG patřily do některé z obecných instrukčních *** práce se zabývá extrakcí grafů toku řízení z bajtkódu jazyka java a následným překladem jednotlivých instrukcí bajtkódu uvnitř základních bloků do instrukční sady LLVM IR. Výsledný program dokáže spolehlivě získat grafy toku řízení z programů v jazyce java zadaných v jakékoli z nejběžnějších forem pro šíření tohoto typu software (.jar archiv, .java nebo .class soubory). Grafy na výstupu jsou navíc koncipovány tak, aby nad nimi bylo možné provádět analýzu za účelem generování jednotkových testů.

关键词： bajtkód jazyka java graf toku řízení analýza LLVM IR java bytecode control flow graph analysis LLVM IR Text

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：