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 条
  • [1] A dynamic logic for the formal verification of java card programs
    Universität Karlsruhe, Institut für Logik, Komplexität und Deduktionssysteme, Karlsruhe
    D-76128, Germany
    [J]. Lect. Notes Comput. Sci, 1600, (6-24):
  • [2] Formalisation and verification of JAVA']JAVA CARD security properties in dynamic logic
    Mostowski, W
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2005, 3442 : 357 - 371
  • [3] Specification and Runtime Verification of Java']Java Card Programs
    da Costa, Umberto Souza
    Moreira, Anamaria Martins
    Musicante, Martin A.
    Souza Neto, Placido A.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 240 : 61 - 78
  • [4] Formal reasoning about non-atomic JAVA']JAVA CARD methods in Dynamic Logic
    Mostowski, Wojciech
    [J]. FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 444 - 459
  • [5] Formal verification of protocol properties of sequential Java']Java programs
    Jin, Ying
    [J]. COMPSAC 2007: THE THIRTY-FIRST ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOL I, PROCEEDINGS, 2007, : 475 - 482
  • [6] Using Krakatoa for Teaching Formal Verification of Java']Java Programs
    Divason, Jose
    Romero, Ana
    [J]. FORMAL METHODS TEACHING (FMTEA 2019), 2019, 11758 : 37 - 51
  • [7] JCML: A specification language for the runtime verification of Java']Java Card programs
    da Costa, Umberto Souza
    Moreira, Anamaria Martins
    Musicante, Martin A.
    Souza Neto, Placid A.
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (04) : 533 - 550
  • [8] Automatic verification of Java']Java programs with dynamic frames
    Smans, Jan
    Jacobs, Bart
    Piessens, Frank
    Schulte, Wolfram
    [J]. FORMAL ASPECTS OF COMPUTING, 2010, 22 (3-4) : 423 - 457
  • [9] Experiences and New Alternatives for Teaching Formal Verification of Java']Java Programs
    Romero, Ana
    Divason, Jose
    [J]. ITICSE'18: PROCEEDINGS OF THE 23RD ANNUAL ACM CONFERENCE ON INNOVATION AND TECHNOLOGY IN COMPUTER SCIENCE EDUCATION, 2018, : 383 - 383
  • [10] Verification of Java']Java bytecode using analysis and transformation of logic programs
    Albert, E.
    Gomez-Zamalloa, M.
    Hubert, L.
    Puebla, G.
    [J]. PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES, 2007, 4354 : 124 - +
12345