Java']Java model checking

被引：15

作者：

Park, DYW ^{[1
]}

Stern, U ^{[1
]}

Skakkebæk, JU ^{[1
]}

Dill, DL ^{[1
]}

机构：

[1] Stanford Univ, Dept Comp Sci, Stanford, CA 94305 USA

来源：

FIFTEENTH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS | 2000年

关键词：

D O I：

10.1109/ASE.2000.873671

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper presents initial results in model checking multi-threaded Java programs. Java programs are translated into the SAL (Symbolic Analysis Laboratory) intermediate language, which supports dynamic constructs such as object instantiations and thread call stacks. The SAL model checker then exhaustively checks the program description for deadlocks and assertion failures, using traditional model checking optimizations to curb the state explosion problem. Most of the advanced features of the Java language are modeled within our framework.

引用

页码：253 / 256

页数：4

共 50 条

[31] Checking and Correcting Behaviors of Java']Java Programs at Runtime with Java']Java-MOP
Chen, Feng
d'Amorim, Marcelo
Rosu, Grigore
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 144 (04) : 3 - 20
[32] Model checking randomized algorithms with Java PathFinder
DisCoVeri Group, Department of Computer Science and Engineering, York University, Toronto, Canada
Proc. - Int. Conf. Quant. Eval. Syst., QEST, (157-158):
[33] A framework for model checking concurrent Java components
School of Maths, Physics and Information Technology, James Cook University , Australia
J. Softw., 2009, 8 (867-874):
[34] Model checking of software components: Combining Java']Java PathFinder and behavior protocol model checker
Parizek, Pavel
Plasil, Frantisek
Kofron, Jan
30TH ANNUAL IEEE/NASA SOFTWARE ENGINEERING WORKSHOP, PROCEEDINGS, 2006, : 133 - +
[35] Towards Model-Checking Security of Real-Time Java']Java Software
Spalazzi, Luca
Spegni, Francesco
Liva, Giovanni
Pinzger, Martin
PROCEEDINGS 2018 INTERNATIONAL CONFERENCE ON HIGH PERFORMANCE COMPUTING & SIMULATION (HPCS), 2018, : 642 - 649
[36] Experience Report: Verifying MPI Java']Java Programs using Software Model Checking
Ayub, Muhammad Sohaib
Rehman, Waqas Ur
Siddiqui, Junaid Haroon
2017 IEEE 28TH INTERNATIONAL SYMPOSIUM ON SOFTWARE RELIABILITY ENGINEERING (ISSRE), 2017, : 294 - 304
[37] TOWARDS MODEL CHECKING WITH JAVA']JAVA PATHFINDER FOR AUTONOMIC SYSTEMS SPECIFIED AND GENERATED WITH ASSL
Vassev, Emil
Hinchey, Mike
Quigley, Aaron
ICSOFT 2009: PROCEEDINGS OF THE 4TH INTERNATIONAL CONFERENCE ON SOFTWARE AND DATA TECHNOLOGIES, VOL 1, 2009, : 251 - +
[38] Symbolic PathFinder: integrating symbolic execution with model checking for Java']Java bytecode analysis
Pasareanu, Corina S.
Visser, Willem
Bushnell, David
Geldenhuys, Jaco
Mehlitz, Peter
Rungta, Neha
AUTOMATED SOFTWARE ENGINEERING, 2013, 20 (03) : 391 - 425
[39] Similarity-Based Search for Model Checking: A Pilot Study with Java']Java PathFinder
Ibrahimov, Elmin
Wang, Jixing
Zhou, Zhi Quan
2013 13TH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE (QSIC), 2013, : 238 - 244
[40] An Approach to Checking Consistency between UML Class Model and Its Java']Java Implementation
Chavez, Hector M.
Shen, Wuwei
France, Robert B.
Mechling, Benjamin A.
Li, Guangyuan
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2016, 42 (04) : 322 - 344

← 1 2 3 4 5 →