What is Proved and What is Assumed | seL4
The Proof This page defines in high-level language what the seL4 proofs demonstrate, what we assume, and what the proof implies. It is aimed at an audience with a technical background, but does not assume any expertise in formal verification. What we prove Formal proofs can be tricky. They prove exactly what you have stated, not necessarily what you mean or what you want. Our proof statement in hi
Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記 (はてなBlog)
昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より： PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか？
Formal methods on some PoS stuff – Yoichi Hirai – Medium
Formal methods on some PoS stuffIn Paris, I received a description of a distributed consensus mechanism. If the description below looks ambiguous or impenetrable, this post is for you. I banged my head to formal verification tools called Alloy and Isabelle/HOL to clarify my understanding (code). Here is the description: Message types:* commit(HASH, view), 0 <= view * prepare(HASH, view, view_sourc
Concrete Semantics
The book Concrete Semantics introduces semantics of programming languages through the medium of a proof assistant. It consists of two parts: Part I is a self-contained introduction to the proof assistant Isabelle. Part II is an introduction to semantics and its applications and is based on a simple imperative programming language. It covers the following topics: operational semantics, compiler cor
Isabelle入門の入門 - Qiita
最近Isabelle始めたばかりなので, 初心者的な視点からIsabelle入門以前の話をします. この記事を読んでIsabelleに興味を持たれたら, 是非公式turtorialからIsabelleへ入門してみてください. Isabelleについて Isabelleは証明支援言語です. 以下にその特徴をあげてみます. 標準のjEdit環境がリッチ 強力な自動証明機構 (とにかく自動証明コマンドが豊富で, さらに証明をIsabelleに探索させることもできます) 公理系が選べる (公理系はライブラリレベルでサポートされています. importするライブラリを自分で選ぶことで, HOL, ZF, Sequents, Cube などなどたくさんの公理系を扱うことができます) Isabelle/Isarによる人間に優しい証明 (Coqのように証明図をコマンドによって変形していくだけでなく, Is
Isabelle/HOL Exercises
Isabelle/HOL Exercises Overview This is a collection of exercises for getting acquainted with the proof assistant Isabelle/HOL. The individual exercises come out of an annual Isabelle/HOL lab course taught at the Technische Universität München. The exercises are arranged theme wise, and as far as possible in order of increasing difficulty. They can be used in conjunction with the online Isabelle/H
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - pandaman64/sabi: Formal semantics of Rust
https://people.eng.unimelb.edu.au/rizkallahc/publications/echronos_verif.pdf
GitHub - data61/PSL
Isabelle/C
PSL/slide/2019_ps.pdf at master · data61/PSL
ソフトウェア開発を工学にする形式手法の紹介 - formal_methods.pdf
TLA+ as an Isabelle object logic
Validating Formal Descriptions of TCP/IP - Experimental Formal Semantics
GitHub - au-ts/cogent: Cogent Project
Eisbach | TS | Data61
Cogent | TS | Data61
AutoCorres: Automatic Specification Abstraction | TS | Data61
Isabelle/ZF sessions (Isabelle2021-1-build)
verified insertino sort by Isabelle