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] Static analysis of Java bytecode
    Zhao, J.-J.
    Wuhan University Journal of Natural Sciences, 6 (1-2): : 383 - 390
  • [2] Java bytecode specification and verification
    Burdy, Lilian
    Pavlova, Mariela
    Proc ACM Symp Appl Computing, 1600, (1835-1839):
  • [3] Model checking real time Java using Java PathFinder
    Lindstrom, Gary
    Mehlitz, Peter C.
    Visser, Willem
    Lect. Notes Comput. Sci., (444-456):
  • [4] Bytecode verification on Java smart cards
    Leroy, Xavier
    Software - Practice and Experience, 2002, 32 (04): : 319 - 340
  • [5] 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):
  • [6] Verifiable control flow policies for Java bytecode
    Fontaine, Arnaud
    Hym, Samuel
    Simplot-Ryl, Isabelle
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2012, 7140 LNCS : 115 - 130
  • [7] Using compressed bytecode traces for slicing java programs
    Wang, Tao
    Roychoudhury, Abhik
    Proceedings - International Conference on Software Engineering, 2004, 26 : 512 - 521
  • [8] Self-healing assurance based on bounded model checking
    Faculty of Information Technology, Brno University of Technology, Božetěchova 2, Brno
    CZ-612 66, Czech Republic
    Lect. Notes Comput. Sci., (295-303):
  • [9] A space-aware bytecode verifier for java cards
    Bernardeschi, Cinzia
    Lettieri, Giuseppe
    Martini, Luca
    Masci, Paolo
    Electron. Notes Theor. Comput. Sci., 1 SPEC. ISS. (237-254):
  • [10] Deterministic execution of Java's primitive bytecode operations
    IPD, Universität Karlsruhe, Am Fasanengarten 5, Karlsruhe
    76128, Germany
    不详
    76131, Germany
    Proc. Java Virtual Mach. Res. Technol. Symp., JVM, 1600,
12345