Deadlock Detection of Java']Java Bytecode

被引：1

作者：

Laneve, Cosimo ^{[1
]}

Garcia, Abel ^{[1
]}

机构：

[1] Univ Bologna, Dept Comp Sci & Engn, Inria Focus, Bologna, Italy

来源：

LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2017) | 2018年 / 10855卷

关键词：

D O I：

10.1007/978-3-319-94460-9_3

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper presents a technique for deadlock detection of Java programs. The technique uses typing rules for extracting infinitestate abstract models of the dependencies among the components of the Java intermediate language - the Java bytecode. Models are sub-sequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is complemented by a prototype verifier that also covers most of the Java features.

引用

页码：37 / 53

页数：17

共 14 条

[1]

Atkey R., 2015, ECE ASST, V72

[2]

Bensalem S, 2006, LECT NOTES COMPUT SC, V3875, P208

[3] Sherlock: Scalable Deadlock Detection for Concurrent Programs [J].

Eslamimehr, Mahdi ;

Palsberg, Jens .

22ND ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING (FSE 2014), 2014, :353-365

[4] Checkmate: a Generic Static Analyzer of Java']Java Multithreaded Programs [J].

Ferrara, Pietro .

SEFM 2009: SEVENTH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2009, :169-178

[5]

Flores-Montoya AE, 2013, LECT NOTES COMPUT SC, V7892, P273

[6]

Garcia A.M., 2017, THESIS

[7]

Giachino Elena, 2014, CONCUR 2014 - Concurrency Theory. 25th International Conference, CONCUR 2014. Proceedings: LNCS 8704, P63, DOI 10.1007/978-3-662-44584-6_6

[8]

Giachino Elena, 2014, Formal Methods for Executable Software Models. 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014. Advanced Lectures: LNCS 8483, P26, DOI 10.1007/978-3-319-07317-0_2

[9] A framework for deadlock detection in core ABS [J].

Giachino, Elena ;

Laneve, Cosimo ;

Lienhardt, Michael .

SOFTWARE AND SYSTEMS MODELING, 2016, 15 (04) :1013-1048

[10] Deadlock analysis of unbounded process networks [J].

Kobayashi, Naoki ;

Laneve, Cosimo .

INFORMATION AND COMPUTATION, 2017, 252 :48-70

← 1 2 →