Machine-checked model for Micro-Dalvik virtual machine

被引：0
|
作者：
He, Yan-Xiang [1 ,2 ]
Jiang, Nan [1 ,3 ]
Li, Qing-An [1 ,2 ]
Zhang, Jun [1 ,4 ]
Shen, Fan-Fan [1 ]
机构：
[1] Computer School, Wuhan University, Wuhan,430072, China
[2] State Key Laboratory of Software Engineering, Wuhan University, Wuhan,430072, China
[3] Computer School, Hubei University of Technology, Wuhan,430068, China
[4] Software College, East China Institute of Technology, Nanchang,330013, China
来源：
Ruan Jian Xue Bao/Journal of Software | 2015年 / 26卷 / 02期
关键词：
Computer programming languages - Virtual machine - Theorem proving - Formal specification - Semantics - Network security;
D O I：
10.13328/j.cnki.jos.004787
中图分类号：
学科分类号：
摘要：
This paper introduces Micro-Dalvik, a formalized Dalvik-like VM model to exhibit core features of the register-based architecture. This formal specification describes the instruction set and runtime state, and the runtime behaviors of the instructions as state transitions based on big-step operational semantics. The Micro-Dalvik VM instruction set is more abstract than comparable Dalvik VM to attain clarity of its semantics, but bears no further simplification of the meaning of instructions. Some properties of Micro-Dalvik VM semantics are stated based on this formal specification and sketch of the proofs is provided. This formalization is implemented in the theorem proof assistant Isabelle/HOL. © Copyright 2015, Institute of Software. the Chinese Academy of Sciences, All Rights Reserved.
引用
收藏
页码：364 / 379
相关论文
共 50 条
  • [1] Formal verification of m java compiler targeting Micro-Dalvik virtual machine
    Jiang N.
    He Y.-X.
    Zhang X.-T.
    1619, Chinese Institute of Electronics (44): : 1619 - 1629
  • [2] A Machine-Checked Model of Safe Composition
    Delaware, Benjamin
    Cook, William
    Batory, Don
    FOAL09: FOUNDATIONS OF ASPECT-ORIENTED LANGUAGES, 2009, : 31 - 35
  • [3] A machine-checked model for a java']java-like language, virtual machine, and compiler
    Klein, Gerwin
    Nipkow, Tobias
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006, 28 (04): : 619 - 695
  • [4] A machine-checked formalization of the random oracle model
    Barthe, G
    Tarento, S
    TYPES FOR PROOFS AND PROGRAMS, 2006, 3839 : 33 - 49
  • [5] A machine-checked formalization of the generic model and the random oracle model
    Barthe, G
    Cederquist, J
    Tarento, S
    AUTOMATED REASONING, PROCEEDINGS, 2004, 3097 : 385 - 399
  • [6] A machine-checked correctness proof for Pastry
    Azmy, Noran
    Merz, Stephan
    Weidenbach, Christoph
    SCIENCE OF COMPUTER PROGRAMMING, 2018, 158 : 64 - 80
  • [7] Machine-checked Verification of Cognitive Agents
    Jensen, Alexander Birch
    ICAART: PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON AGENTS AND ARTIFICIAL INTELLIGENCE - VOL 1, 2022, : 245 - 256
  • [8] Machine-Checked Semantic Session Typing
    Hinrichsen, Jonas Kastberg
    Louwrink, Daniel
    Krebbers, Robbert
    Bengtson, Jesper
    CPP '21: PROCEEDINGS OF THE 10TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2021, : 178 - 198
  • [9] Java and the java memory model - A unified, machine-checked formalisation
    Karlsruher Institut für Technologie, Germany
    Lect. Notes Comput. Sci., (497-517):
  • [10] A Machine-Checked Framework for Relational Separation Logic
    Manuel Crespo, Juan
    Kunz, Cesar
    SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 122 - 137
12345