Mapped Separation Logic

被引：0
|
作者：
Kolanski, Rafal [1 ,2 ]
Klein, Gerwin [1 ,2 ]
机构：
[1] NICTA, Sydney Res Lab, Sydney, NSW, Australia
[2] UNSW, Sch Comp Sci & Engn, Sydney, NSW, Australia
来源：
VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS | 2008年 / 5295卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present Mapped Separation Logic, an instance of Separation Logic for reasoning about virtual memory. Our logic is formalised in the Isabelle/HOL theorem prover and it allows reasoning on properties about page tables, direct physical memory access, virtual memory access, and shared memory. Mapped Separation Logic fully supports all rules of abstract Separation Logic, including the frame rule.
引用
收藏
页码：15 / +
页数：2
相关论文
共 50 条
  • [1] Fast Boolean Logic Mapped on Memristor Crossbar
    Xie, Lei
    Hoang Anh Du Nguyen
    Taouil, Mottaqiallah
    Hamdioui, Said
    Bertels, Koen
    [J]. 2015 33RD IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN (ICCD), 2015, : 335 - 342
  • [2] EA-based refactoring of mapped logic circuits
    Kocnova, Jitka
    Vasicek, Zdenek
    [J]. 2019 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS (ISCAS), 2019,
  • [3] Distributed Reasoning for Mapped Ontologies Using Rewriting Logic
    Bourahla, Mustapha
    [J]. Model and Data Engineering, 2016, 9893 : 142 - 155
  • [4] Separation Logic
    O'Hearn, Peter
    [J]. COMMUNICATIONS OF THE ACM, 2019, 62 (02) : 86 - 95
  • [5] The Logic of Separation Logic: Models and Proofs
    de Boer, Frank S.
    Hiep, Hans-Dieter A.
    de Gouw, Stijn
    [J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2023, 2023, 14278 : 407 - 426
  • [6] Hybrid Threshold-Boolean Logic Mapped on Memristor Crossbar
    Xie, Lei
    [J]. 2016 12TH CONFERENCE ON PH.D. RESEARCH IN MICROELECTRONICS AND ELECTRONICS (PRIME), 2016,
  • [7] Relational separation logic
    Yang, Hongseok
    [J]. THEORETICAL COMPUTER SCIENCE, 2007, 375 (1-3) : 308 - 334
  • [8] Fictional Separation Logic
    Jensen, Jonas Braband
    Birkedal, Lars
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, 2012, 7211 : 377 - 396
  • [9] Algebraic separation logic
    Dang, H. -H.
    Hoefner, P.
    Moeller, B.
    [J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2011, 80 (06): : 221 - 247
  • [10] An overview of separation logic
    Reynolds, John C.
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 460 - 469
12345