You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert
We continue our work on formal verification of Rust programs with our tool coq-of-rust, to translate Rust code to the formal proof system Coq. One of the limitation we had was the handling of primitive constructs from the standard library of Rust, like Option::unwrap_or_default or all other primitive functions. For each of these functions, we had to make a Coq definition to represent its behavior.
はじめにCoqで解析入門の1章にある命題を全て証明してみたので記事を書いてみます。 Coqでの証明大学で記号論理学の授業を受けたことはありますか?記号論理学では数学の命題を証明木を用いて形式的証明をしていましたがCoqでも形式的証明をします。流れは以下です。 数学の命題を論理記号で書きますゴールが表示されるので適切にCoqのTacticを使いますするとゴールが変わるので未証明のゴールがなくなるまで繰り返しTacticを使います Coqでの証明の魅力は 証明が正しいことをCoqが保証してくれること(Coqにバグがあるかもしれませんが多分)証明した定理が他の定理の証明に使えて楽しいところ などです。 やろうと思った背景大学1年生の頃、解析入門を前から読んで途中で理解できなくなって読み直すというのを繰り返していました。 いつか理解したいなと思っていたときに記号論理学の授業を受けて解析入門の証明も
こんにちは、チェシャ猫です。先日行われた第 7 回 Web System Architecture 研究会で形式手法について発表してきました。 普段、形式手法について登壇する際は具体例な検証例を出すことが多いですが、今回は理論側に寄せたサーベイになっています。 はじめに 本セッションでは、安全性-活性分解 (safety-liveness decomposition) と呼ばれる一連の結果について解説する。安全性-活性分解は、システムの仕様が与えられた時、それを安全性 (safety) および活性 (liveness) と呼ばれる、よりシンプルな特徴付けを持つクラスに分解して扱うための方法論である。さらにセッションの後半では、安全性と活性の組み合わせ以外にも提案されている派生的な特徴付けについても述べる。 Web アプリケーションと形式手法 システムやプログラムの性質を何らかの数学的な対象
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these ex
形式手法の導入を検討する上で参考となる実システムに対する実践的な応用事例について、費用対効果や導入時の課題・工夫点等を中心にまとめています。 現在は、「フォーマルメソッド導入ガイダンス」第4部付録 12.応用事例情報 と同じ内容ですが、今後事例の数を増やしていく予定です。 キーワードで検索する
2020年1月に入社し、SWETの仕様分析サポートチームに加わったtakasek(@takasek)です。 仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています(形式手法 カテゴリーの記事一覧)。 この記事では、加入3か月を経てようやく形式手法の輪郭が掴めてきた私の視点から、学習前後での理解の変化について振り返ります。想定読者として学習前の私と近い属性——すなわちコンピュータサイエンスや数学の専門教育を受けておらず、主に現場での実務と自習に頼ってきたソフトウェアエンジニアを想定しています。 形式手法を学ぶ前の認識と疑問 ソフトウェアエンジニアとしての私の一番の興味関心は設計手法です。設計は、なんらかの解決したい問題に対して、ある一面を切り取った構造(モデル)を与え、そのモデルを解決の機構に落
英語版記事を日本語へ機械翻訳したバージョン(Google翻訳)。 万が一翻訳の手がかりとして機械翻訳を用いた場合、翻訳者は必ず翻訳元原文を参照して機械翻訳の誤りを訂正し、正確な翻訳にしなければなりません。これが成されていない場合、記事は削除の方針G-3に基づき、削除される可能性があります。 信頼性が低いまたは低品質な文章を翻訳しないでください。もし可能ならば、文章を他言語版記事に示された文献で正しいかどうかを確認してください。 履歴継承を行うため、要約欄に翻訳元となった記事のページ名・版について記述する必要があります。記述方法については、Wikipedia:翻訳のガイドライン#要約欄への記入を参照ください。 翻訳後、{{翻訳告知|en|Boolean satisfiability problem|…}}をノートに追加することもできます。 Wikipedia:翻訳のガイドラインに、より詳細な
計算機科学における正当性(Correctness)とは、アルゴリズムがその仕様に照らして正しいことを意味する。「機能的」正当性とは、アルゴリズムの入出力動作に関する正当性である(すなわち、各入力に対して正しく出力を生成すること)。形式的検証を参照されたい。 完全正当性(Total Correctness)は、アルゴリズムが常に停止することも要求される。一方、部分正当性(Partial Correctness)は単に返ってくる答えが正しいことのみを要求する(常に答えが返ってくるとは限らない)。停止問題には汎用的解法はないので、完全正当性はより深い問題をはらんでいる。 例えば、整数を 1 から順に調べて奇数の完全数を探すとした場合、部分正当性を備えたプログラムを書くのは極めて簡単である(素因数分解を行って n が完全数かどうかを調べる)。しかし、そのプログラムが完全正当性を備えているとするには
About CakeML is a functional programming language and an ecosystem of proofs and tools built around the language. The ecosystem includes a proven-correct compiler that can bootstrap itself. The CakeML project consists of the following components, all of which are free software. Language definition. The CakeML language is based on a substantial subset of Standard ML. Its formal semantics is specifi
Z言語 (ぜっどげんご) は、Z記法 (ぜっどきほう) ともいい、形式仕様記述言語であり、コンピュータシステムの記述とモデリングを行うために使われる。 ZはZF集合論から名前をとって命名された。 Zは次のことに焦点を当てている。 コンピュータプログラムの簡明な仕様の記述。 意図するプログラムの振る舞いの証明の形式化。 Zは、もともとは1977年に Jean-Raymond Abrial により Steve Schuman とバートランド・メイヤーの支援を得て開発された[1]。 Zの開発は、オクスフォード大学のプログラミング研究グループでさらに続けられた。 Abrial は、1980年前半にこの研究グループで開発作業を行った。 Zは、公理的集合論とラムダ計算、一階述語論理で使われる標準的な数学的記法に基づいている。 Zで記述されたあらゆる式は型づけられており、それにより素朴集合論のパラドック
Overview SyncStitch is a model checker based on the process algebra CSP (Communicating Sequential Processes). By using SyncStitch, you can check six types of properties of the system you are developping: Deadlocks Divergences (also known as livelocks) Refinement relation on traces semantics (safety) Refinement relation on stable failures semantics (safety and liveness) LTL (Linear-Time Logic) with
What is Isabelle? Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle ov
The Isabelle[a] automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects. Isabelle is available inside a flexible system framework allowing for logically safe extensions, wh
Developers Summit 2020 で使用したスライドです。 言葉というものは曖昧です。複数人が「ともにつくる」システムにおいて、メンバ間で仕様を正しく共有することは非常に重要ですが、一方で言葉の裏側に隠された「暗黙の仮定」を見抜くことは簡単ではありません。このような仕様の曖昧性への対抗手段として、本セッションでは「形式手法」を紹介します。形式手法ではシステムの挙動を数学的に記述することにより、自然言語の持つ曖昧性を排除し、仕様が満たされるかどうかを厳密に検証することが可能になります。あなたの頭の中にある仕様がどのように「数学的な記述」に変換されるのか、具体例を通して体験してみませんか? イベント概要:https://event.shoeisha.jp/devsumi/20200213/session/2380/
2019年が終わろうとしています あけおめ~さて2020年になりました。歴史が長い形式手法の今後を占うため、過去と直近の出来事を振り返りたいと思います。 ツッコミやタレコミは私のTwitter宛かあなたのブログかその他経路でお願いします~ シンボリック実行は形式的であるため本稿では形式手法に含めることにします。 Fuzzing関連はサーベイが甘いので漏れが多いかもしれません。 形式手法・形式検証とは 形式検証とは、厳密に定義された意味論の下で仕様やプログラムが所定の性質を満たすことを形式的に検証するための手法をいいます。「形式的に」とは、検証が事前に定義された知識だけに基づいており、検証手順が決定的であることをいうと私は理解しています。 形式手法は、形式検証に加えて、形式的にプログラムの仕様を厳密に定義するための手法を包含します。 本記事では形式手法を以下の通り大きく3つに独自に分類します
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く