Experience Report: seL4 Formally Verifying a High-Performance Microkernel

被引：5
|
作者：
Klein, Gerwin
Derrin, Philip
Elphinstone, Kevin
机构：
来源：
ACM SIGPLAN NOTICES | 2009年 / 44卷 / 8-9期
关键词：
Verification; Design; Languages; Haskell; seL4; microkernel; Isabelle/HOL;
D O I：
10.1145/1631687.1596566
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. The verification connects an abstract operational specification in the theorem prover Isabelle/HOL to a C implementation of the microkernel. We describe how this project differs from other efforts, and examine the effect of using Haskell in a large-scale formal verification. The kernel comprises 8,700 lines of C code; the verification more than 150,000 lines of proof script.
引用
收藏
页码：91 / 95
页数：5
相关论文
共 50 条
  • [21] High-performance 4H-SiC junction barrier Schottky diodes with double resistive termination extensions
    Zheng Liu
    Zhang Feng
    Liu Sheng-Bei
    Dong Lin
    Liu Xing-Fang
    Fan Zhong-Chao
    Liu Bin
    Yan Guo-Guo
    Wang Lei
    Zhao Wan-Shun
    Sun Guo-Sheng
    He Zhi
    Yang Fu-Hua
    CHINESE PHYSICS B, 2013, 22 (09)
  • [22] Preparation of Three-Dimensional Co3O4/graphene Composite for High-Performance Supercapacitors
    Yang, MinHo
    Choi, Bong Gill
    CHEMICAL ENGINEERING COMMUNICATIONS, 2017, 204 (07) : 723 - 728
  • [23] High-performance alpha-voltaic cell based on a 4H-SiC PIN junction diode
    Gao, Runlong
    Liu, Linyue
    Li, Yang
    Shen, Lvkang
    Wan, Pengying
    Ouyang, Xiao
    Zhang, Haozhe
    Ruan, Jinlu
    Zhou, Leidang
    Chen, Liang
    Zhang, Xianpeng
    Liu, Jinliang
    Li, Hui
    Liu, Ming
    Ouyang, Xiaoping
    ENERGY CONVERSION AND MANAGEMENT, 2022, 252
  • [24] Implementing High-performance Complex Matrix Multiplication via the 3m and 4m Methods
    Van Zee, Field G.
    Smith, Tyler M.
    ACM TRANSACTIONS ON MATHEMATICAL SOFTWARE, 2017, 44 (01):
  • [25] Nanostructure NiCo2S4 with different morphologies grown on Ni foam for high-performance supercapacitors
    Xiao, Xuechun
    Han, Enshan
    Zeng, Zhenzhen
    Zhu, Lingzhi
    Li, Ling
    Liu, Zheng
    IONICS, 2019, 25 (07) : 3331 - 3339
  • [26] A porous MOF-derived NiMn2O4 material and its superior energy storage performance for high-performance supercapacitors
    Yuan, Hao
    Yuming, Guo
    Jiang, Linghong
    NEW JOURNAL OF CHEMISTRY, 2022, 46 (12) : 5741 - 5750
  • [27] Hierarchical NiCo2O4@NiCo2O4 Core/Shell Nanoflake Arrays as High-Performance Supercapacitor Materials
    Liu, Xiayuan
    Shi, Shaojun
    Xiong, Qinqin
    Li, Lu
    Zhang, Yijun
    Tang, Hong
    Gu, Changdong
    Wang, Xiuli
    Tu, Jiangping
    ACS APPLIED MATERIALS & INTERFACES, 2013, 5 (17) : 8790 - 8795
  • [28] NiCo2O4 nanosheet supported hierarchical core-shell arrays for high-performance supercapacitors
    Zhou, Weiwei
    Kong, Dezhi
    Jia, Xingtao
    Ding, Chunyan
    Cheng, Chuanwei
    Wen, Guangwu
    JOURNAL OF MATERIALS CHEMISTRY A, 2014, 2 (18) : 6310 - 6315
  • [29] Multifunctional G@UC3N4 modified separator for high-performance Li-S batteries
    Tian, Jingkun
    Xu, Songshi
    Zhang, Peng
    Ji, Guangmin
    Gao, Qiqian
    Yang, Yingying
    Xing, Fei
    MICRO AND NANOSTRUCTURES, 2023, 182
  • [30] Hydrothermal synthesis of Mn-doped ZnCo2O4 electrode material for high-performance supercapacitor
    Mary, A. Juliet Christina
    Bose, A. Chandra
    APPLIED SURFACE SCIENCE, 2017, 425 : 201 - 211
12345