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 条
  • [41] JET: Exception Checking in the Java']Java Native Interface
    Li, Siliang
    Tan, Gang
    ACM SIGPLAN NOTICES, 2011, 46 (10) : 345 - 357
  • [42] Types for atomicity: Static checking and inference for Java']Java
    Flanagan, Cormac
    Freund, Stephen N.
    Lifshin, Marina
    Qadeer, Shaz
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2008, 30 (04):
  • [43] JET: Exception Checking in the Java']Java Native Interface
    Li, Siliang
    Tan, Gang
    OOPSLA 11: PROCEEDINGS OF THE 2011 ACM INTERNATIONAL CONFERENCE ON OBJECT ORIENTED PROGRAMMING SYSTEMS LANGUAGES AND APPLICATIONS, 2011, : 345 - 357
  • [44] Optimizing array reference checking in Java']Java programs
    Midkiff, SP
    Moreira, JE
    Snir, M
    IBM SYSTEMS JOURNAL, 1998, 37 (03) : 409 - 453
  • [45] Evaluation of A Tool for Java']Java Structural Specification Checking
    Dil, Anton
    Osunde, Joseph
    PROCEEDINGS OF THE 10TH INTERNATIONAL CONFERENCE ON EDUCATION TECHNOLOGY AND COMPUTERS (ICETC 2018), 2018, : 99 - 104
  • [46] JBMC: A Bounded Model Checking Tool for Java Bytecode
    Brenguier, Romain
    Cordeiro, Lucas
    Kroening, Daniel
    Schrammel, Peter
    arXiv, 2023,
  • [47] JCWIT: A Correctness-Witness Validator for Java']Java Programs Based on Bounded Model Checking
    Cheng, Zaiyu
    Wu, Tong
    Schrammel, Peter
    Tihanyi, Norbert
    de Lima Filho, Eddie B.
    Cordeiro, Lucas C.
    PROCEEDINGS OF THE 33RD ACM SIGSOFT INTERNATIONAL SYMPOSIUM ON SOFTWARE TESTING AND ANALYSIS, ISSTA 2024, 2024, : 1831 - 1835
  • [48] CoffeeStrainer - Statically checking structural constraints on Java']Java programs
    Bokowski, B
    OBJECT-ORIENTED TECHNOLOGY: ECOOP'98 WORKSHOP READER, 1998, 1543 : 380 - 381
  • [49] Checking Access to Protected Members in the Java']Java Virtual Machine
    Coglio, Alessandro
    JOURNAL OF OBJECT TECHNOLOGY, 2005, 4 (08): : 55 - 76
  • [50] Tool demonstration: CHET: Checking specifications in Java']Java systems
    Reiss, SP
    13TH INTERNATIONAL WORKSHOP ON PROGRAM COMPREHENSION, PROCEEDINGS, 2005, : 165 - 168
12345