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 条
  • [1] Model checking the Java']Java metalocking algorithm
    Basu, Samik
    Smolka, Scott A.
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (03) : C1 - C35
  • [2] Model checking programs with Java']Java PathFinder
    Visser, W
    Mehlitz, P
    MODEL CHECKING SOFTWARE, PROCEEDINGS, 2005, 3639 : 27 - 27
  • [3] Applying model checking in Java']Java verification
    Havelund, K
    Skakkebæk, JU
    THEORETICAL AND PRACTICAL ASPECTS OF SPIN MODEL CHECKING, 1999, 1680 : 216 - 231
  • [4] Heuristic model checking for Java']Java programs
    Groce, A
    Visser, W
    MODEL CHECKING SOFTWARE, PROCEEDINGS, 2002, 2318 : 242 - 245
  • [5] Model checking real time Java']Java using Java']Java PathFinder
    Lindstrom, G
    Mehlitz, PC
    Visser, W
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2005, 3707 : 444 - 456
  • [6] Java']Java Memory Model-Aware Model Checking
    Jin, Huafeng
    Yavuz-Kahveci, Tuba
    Sanders, Beverly A.
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2012, 2012, 7214 : 220 - 236
  • [7] Model checking JAVA programs using JAVA PathFinder
    Havelund K.
    Pressburger T.
    International Journal on Software Tools for Technology Transfer, 2000, 2 (4) : 366 - 381
  • [8] Probabilistic Model Checking of Randomized Java']Java Code
    Fatmi, Syyeda Zainab
    Chen, Xiang
    Dhamija, Yash
    Wildes, Maeve
    Tang, Qiyi
    van Breugel, Franck
    MODEL CHECKING SOFTWARE (SPIN 2021), 2021, 12864 : 157 - 174
  • [9] Combining Model Learning and Model Checking to Analyze Java']Java Libraries
    Ali, Shahbaz
    Sun, Hailong
    Zhao, Yongwang
    STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD (SOFL+MSVL 2019), 2020, 12028 : 259 - 278
  • [10] A JPSL Based Model Checking Approach for Java']Java Programs
    Shu, XinFeng
    Li, YanLin
    Gao, WeiRan
    STRUCTURED OBJECT-ORIENTED FORMAL LANGUAGE AND METHOD, SOFL+MSVL 2022, 2023, 13854 : 30 - 49
12345