A dynamic Logic for the formal verification of Java']Java Card programs

被引：0
|
作者：
Beckert, B [1 ]
机构：
[1] Univ Karlsruhe, Inst Log Komplexitat & Dedukt Syst, D-76128 Karlsruhe, Germany
来源：
JAVA ON SMART CARDS: PROGRAMMING AND SECURITY | 2001年 / 2041卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
In this paper, we define a program logic (an instance of Dynamic Logic) for formalising properties of JAVA CARD programs, and we give a sequent calculus for formally verifying such properties. The purpose of this work is to provide a framework for software verification that can be integrated into real-world software development processes.
引用
收藏
页码：6 / 24
页数：19
相关论文
共 50 条
  • [41] Formal Verification of a Java']Java Component Using the RESOLVE Framework
    Rumreich, Laine
    Sivilotti, Paolo A. G.
    [J]. FRONTIERS OF COMBINING SYSTEMS (FROCOS 2021), 2021, 12941 : 287 - 305
  • [42] Dynamic logic for Java
    Beckert, Bernhard
    Klebanov, Vladimir
    Weiß, Benjamin
    [J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2016, 10001 LNCS : 49 - 106
  • [43] Formal techniques for Java']Java-Like programs (FTfJP)
    Coglio, A
    Huisman, M
    Kiniry, JR
    Müller, P
    Poll, E
    [J]. OBJECT-ORIENTED TECHNOLOGY, 2004, 3344 : 76 - 83
  • [44] Using contour marking bytecode verification algorithm on the java']java card
    Jiang, Longlong
    Li, Daiping
    [J]. MECHATRONICS ENGINEERING, COMPUTING AND INFORMATION TECHNOLOGY, 2014, 556-562 : 4120 - +
  • [45] Dynamic Purity Analysis for Java']Java Programs
    Xu, Haiying
    Pickett, Christopher J. F.
    Verbrugge, Clark
    [J]. PASTE'07 PROCEEDINGS OF THE 2007 ACM SIGPLAN- SIGSOFT WORKSHOP ON PROGRAM ANALYSIS FOR SOFTWARE TOOLS & ENGINEERING, 2007, : 75 - 82
  • [46] Dynamic slicing of Java']Java bytecode programs
    Szegedi, A
    Gyimóthy, T
    [J]. FIFTH IEEE INTERNATIONAL WORKSHOP ON SOURCE CODE ANALYSIS AND MANIPULATION, PROCEEDINGS, 2005, : 35 - 44
  • [47] Distributed dynamic slicing of Java']Java programs
    Mohapatra, Durga P.
    Kumar, Rajeev
    Mall, Rajib
    Kumar, D. S.
    Bhasin, Mayank
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2006, 79 (12) : 1661 - 1678
  • [48] No Java']Java without caffeine -: A tool for dynamic analysis of Java']Java programs
    Guéhéneuc, YG
    Douence, R
    Jussien, N
    [J]. ASE 2002: 17TH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, 2002, : 117 - 126
  • [49] A program logic for handling JAVA']JAVA CARD's transaction mechanism
    Beckert, B
    Mostowski, W
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2003, 2621 : 246 - 260
  • [50] On-Device Control Flow Verification for Java']Java Programs
    Fontaine, Arnaud
    Hym, Samuel
    Simplot-Ryl, Isabelle
    [J]. ENGINEERING SECURE SOFTWARE AND SYSTEMS, 2011, 6542 : 43 - 57
12345