Treffer: CIL to Java-bytecode translation for static analysis leveraging
Title:
CIL to Java-bytecode translation for static analysis leveraging
Authors:
Contributors:
Stefania Gnesi, Nico Plat, Paola Spoletini, Patrizio Pelliccione, Ferrara, Pietro, Cortesi, Agostino, Spoto, Nicola Fausto
Publisher Information:
ACM
USA
USA
Publication Year:
2018
Collection:
Università degli Studi di Verona: Catalogo dei Prodotti della Ricerca (IRIS)
Subject Terms:
Document Type:
Konferenz
conference object
File Description:
ELETTRONICO
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/isbn/978-1-4503-5718-0; info:eu-repo/semantics/altIdentifier/wos/WOS:000521511000001; ispartofbook:Proceedings of the 6th Conference on Formal Methods in Software Engineering, FormaliSE 2018; 6th Conference on Formal Methods in Software Engineering, FormaliSE 2018; firstpage:40; lastpage:49; numberofpages:10; alleditors:Stefania Gnesi, Nico Plat, Paola Spoletini, Patrizio Pelliccione; https://hdl.handle.net/11562/988470; https://dl.acm.org/citation.cfm?doid=3193992.3193994
DOI:
10.1145/3193992.3193994
Availability:
Rights:
info:eu-repo/semantics/restrictedAccess
Accession Number:
edsbas.73ED327
Database:
BASE
Weitere Informationen
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.