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 条
  • [21] Verification of MPI Java']Java Programs using Software Model Checking
    Rehman, Waqas Ur
    Ayub, Muhammad Sohaib
    Siddiqui, Junaid Haroon
    ACM SIGPLAN NOTICES, 2016, 51 (08) : 413 - 414
  • [22] JBMC: Bounded Model Checking for Java']Java Bytecode (Competition Contribution)
    Cordeiro, Lucas
    Kroening, Daniel
    Schrammel, Peter
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, 2019, 11429 : 219 - 223
  • [23] Model checking a cache coherence protocol of a Java']Java DSM implementation
    Pang, Jun
    Fokkink, Wan
    Hofman, Rutger
    Veldema, Ronald
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2007, 71 (01): : 1 - 43
  • [24] A Java']Java Code Annotation Approach for Model Checking Software Systems
    Ferreira, Glauber
    Loureiro, Emerson
    Oliveira, Elthon
    APPLIED COMPUTING 2007, VOL 1 AND 2, 2007, : 1536 - 1537
  • [25] Using runtime analysis to guide model checking of Java']Java programs
    Havelund, K
    SPIN MODEL CHECKING AND SOFTWARE VERIFICATON, 2000, 1885 : 245 - 264
  • [26] JBMC: A Bounded Model Checking Tool for Verifying Java']Java Bytecode
    Cordeiro, Lucas
    Kesseli, Pascal
    Kroening, Daniel
    Schrammel, Peter
    Trtik, Marek
    COMPUTER AIDED VERIFICATION (CAV 2018), PT I, 2018, 10981 : 183 - 190
  • [27] Model-checking multi-threaded distributed Java']Java programs
    Stoller, SD
    SPIN MODEL CHECKING AND SOFTWARE VERIFICATON, 2000, 1885 : 224 - 244
  • [28] Platform-Specific Restrictions on Concurrency in Model Checking of Java']Java Programs
    Parizek, Pavel
    Kalibera, Tomas
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2009, 5825 : 117 - 132
  • [29] Byte code verification for Java']Java smart cards based on model checking
    Posegga, J
    Vogt, H
    COMPUTER SECURITY - ESORICS 98, 1998, 1485 : 175 - 190
  • [30] Signalling integer overflows in Java']Java - A tool for checking overflows in Java']Java code
    Bapst, Frederic
    Kilchoer, Francois
    DR DOBBS JOURNAL, 2008, 33 (09): : 54 - 58
12345