CIL to Java']Java-bytecode Translation for Static Analysis Leveraging

被引：2
|
作者：
Ferrara, Pietro [1 ]
Cortesi, Agostino [2 ]
Spoto, Fausto [3 ]
机构：
[1] JuliaSoft SRL, Verona, Italy
[2] Univ Ca Foscari Venezia, Venice, Italy
[3] Univ Verona, Verona, Italy
来源：
2018 ACM/IEEE CONFERENCE ON FORMAL METHODS IN SOFTWARE ENGINEERING (FORMALISE 2018) | 2018年
关键词：
D O I：
10.1145/3193992.3193994
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
A formal translation of CIL (i.e., .Net) bytecode into Java bytecode is introduced and proved sound with respect to the language semantics. The resulting code is then analyzed with Julia, an industrial static analyzer of Java bytecode. The overall process of translation and analysis is fast, scales up to industrial programs, and introduces a negligible number of false alarms. The main result of this work is to leverage existing, mature, and sound analyzers for Java bytecode by applying them to the (translated) CIL bytecode.
引用
收藏
页码：40 / 49
页数：10
相关论文
共 50 条
  • [1] From CIL to Java']Java bytecode: Semantics-based translation for static analysis leveraging
    Ferrara, Pietro
    Cortesi, Agostino
    Spot, Fausto
    SCIENCE OF COMPUTER PROGRAMMING, 2020, 191
  • [2] Static Analysis of Java Bytecode
    Jian\|jun Zhao Department of Computer Science and Engineering
    Wuhan University Journal of Natural Sciences, 2001, (Z1) : 383 - 390
  • [3] Static analysis of Java bytecode
    Zhao, J.-J.
    Wuhan University Journal of Natural Sciences, 6 (1-2): : 383 - 390
  • [4] An Evaluation of Static Java']Java Bytecode Watermarking
    Hamilton, James
    Danicic, Sebastian
    WORLD CONGRESS ON ENGINEERING AND COMPUTER SCIENCE, VOLS 1 AND 2, 2010, : 1 - 8
  • [5] A Comparative Analysis of Static and Dynamic Java']Java Bytecode Watermarking Algorithms
    Kumar, Krishan
    Kaur, Prabhpreet
    SOFTWARE ENGINEERING (CSI 2015), 2019, 731 : 319 - 334
  • [6] Efficient inference of static types for Java']Java bytecode
    Gagnon, EM
    Hendren, LJ
    Marceau, G
    STATIC ANALYSIS, 2000, 1824 : 199 - 219
  • [7] Static Resource Analysis for Java']Java Bytecode Using Amortisation and Separation Logic
    Fenacci, Damon
    MacKenzie, Kenneth
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 279 (01) : 19 - 32
  • [8] Termination analysis of Java']Java Bytecode
    Albert, Elvira
    Arenas, Puri
    Codish, Michael
    Genaim, Samir
    Puebla, German
    Zanardini, Damiano
    FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, 2008, 5051 : 2 - +
  • [9] Cost analysis of Java']Java bytecode
    Albert, E.
    Arenas, P.
    Genaim, S.
    Puebla, G.
    Zanardini, D.
    PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2007, 4421 : 157 - +
  • [10] Dependence analysis of Java']Java bytecode
    Zhao, JJ
    24TH ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COSPSAC 2000), 2000, 24 : 486 - 491
12345