[B! c][coq] masterqのブックマーク

masterq id:masterq

cとcoqに関するmasterqのブックマーク (9)

The Pip Protokernel
masterq 2024/11/27
"The logic of Pip is implemented in Gallina — the language of the Coq proof assistant — and it is in the process of being equipped with a formal proof that it ensures memory isolation. For efficiency, it is automatically translated into freestanding C code."

coq

proof

verify

kernel

c

あとで読む

os
リンク
Verifiable C
masterq 2021/07/03
こんなのがあったんだ。読まねば

あとで読む

doc

coq

verify

c

language
リンク
A Formal C Memory Model for Separation Logic - Journal of Automated Reasoning
masterq 2018/08/23
verify

seplog

memory

c

c11

coq
リンク
Verifiable C
Verifiable C is a program logic for the C programming language: foundational higher-order impredicative concurrent separation logic, proved sound with respect to the operational semantics of CompCert C
masterq 2018/06/01
これも調べないと

c

language

seplog

verify

coq
リンク
PowerPoint プレゼンテーション
Ruby Extension Library Verified using Coq Proof-assistant Tanaka Akira National Institute of Advanced Industrial Science and Techno logy (AIST) RubyKaigi 2017 2017-09-20 2 About This Talk • Formal verification for fast & safe program in C • Quality assurance other than test 3 Materials • Ruby • Coq • C • HTML escape • Intel SSE Do you know all of them? 4 Coq Proof-assistant • Proof assistant – Prog
masterq 2017/09/20
sse

intel

simd

coq

c

ruby

verify
リンク
CoqからのCプログラム生成田中哲産業技術総合研究所情報技術研究部門 2017-07-23 Proof Summit 2017
CoqからのCプログラム生成田中哲産業技術総合研究所情報技術研究部門 2017-07-23 Proof Summit 2017 2/48 元ネタ ● 既発表の話です ● そのうち論文が出ます ● Safe Low-level Code Generation in Coq using Monomorphization and Monadification Akira Tanaka, Reynald Affeldt, Jacques Garrigue IPSJ SIGPRO 114, 2017-06-09, will be appear at IPSJ JIP. ● ここで出てくる plugin は github にあります – https://github.com/akr/monomorphization – https://github.com/akr/monadification
masterq 2017/07/23
coq

c

language
リンク
The Pip Protokernel
masterq 2017/05/01
わずか9つしかシステムコールのないkernel。ユーザ空間の上でLinuxとFreeRTOSが同時に動く。今はx86実装のみ。Xenのさらに薄い版みたいな感じ？Coqで証明済み。副作用はモナドで抽象化し、ポインタ使用も安全だとのこと

verify

c

coq

monad

pip

protokernel

linux

freertos

os

kernel
リンク
GitHub - 2xs/digger
masterq 2017/04/29
coq

c

translation

compile
リンク
CompCert - Main page
The CompCert project investigates the formal verification of realistic compilers usa ble for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees
masterq 2010/12/25
coq

c

proof
リンク
1