JBMC: A Bounded Model Checking Tool for Java Bytecode

被引：0
|
作者：
Brenguier, Romain [1 ]
Cordeiro, Lucas [2 ]
Kroening, Daniel [1 ,3 ]
Schrammel, Peter [1 ,4 ]
机构：
[1] Diffblue Ltd, United Kingdom
[2] University of Manchester, United Kingdom
[3] University of Oxford, United Kingdom
[4] University of Sussex, Brighton, United Kingdom
来源：
arXiv | 2023年
关键词：
Compendex;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
Semantics
引用
收藏
相关论文
共 50 条
  • [1] 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
  • [2] 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
  • [3] A local approach for temporal model checking of Java']Java bytecode
    Santone, A
    Vaglini, G
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2005, 70 (02) : 258 - 281
  • [4] 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
  • [5] Checking secure information flow in Java']Java bytecode by code transformation and standard bytecode verification
    Bernardeschi, C
    De Francesco, N
    Lettieri, G
    Martini, L
    SOFTWARE-PRACTICE & EXPERIENCE, 2004, 34 (13): : 1225 - 1255
  • [6] Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis
    Corina S. Păsăreanu
    Willem Visser
    David Bushnell
    Jaco Geldenhuys
    Peter Mehlitz
    Neha Rungta
    Automated Software Engineering, 2013, 20 : 391 - 425
  • [7] Bytecode verification by model checking
    ETH Zürich, Zürich, Switzerland
    不详
    不详
    Basin, D., 1600, Kluwer Academic Publishers (30): : 3 - 4
  • [8] Bytecode Verification by Model Checking
    David Basin
    Stefan Friedrich
    Marek Gawkowski
    Journal of Automated Reasoning, 2003, 30 : 399 - 444
  • [9] Bytecode verification by model checking
    Basin, D
    Friedrich, S
    Gawkowski, M
    JOURNAL OF AUTOMATED REASONING, 2003, 30 (3-4) : 399 - 444
  • [10] BlueCov: Integrating Test Coverage and Model Checking with JBMC
    Guedemann, Matthias
    Schrammel, Peter
    38TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, SAC 2023, 2023, : 1695 - 1697
12345