PRINCIPIA
Products
Seminar
About Us
セミナー
現在予定されているセミナーにつきましては
CONNPASS のページ
をご覧ください.
セミナー開催のリクエストは isaac@principia-m.com までご連絡ください.
並行システム・プロセス代数 CSP・SyncStitch
並行システムの設計検証
デッドロック発見器を作って学ぶマルチスレッドプログラミング ★共有変数編★
デッドロック発見器を作って学ぶマルチスレッドプログラミング ★メッセージ通信編★
モデル検査器を作って学ぶマルチスレッドプログラミング
トレース比較器を作って学ぶマルチスレッドプログラミング
リファインメント検査器を作って学ぶマルチスレッドプログラミング
アクターモデルに基づく並行合成器と分散システムの合意問題への適用例
ロックフリーアルゴリズムのモデル化と分析
プロセス代数 CSP 構文と操作的意味論
条件変数のモデル化と分析の例
x86-TSO メモリモデルの分析
形式検証・定理証明・Isabelle・Coq
プログラムの正しさを数学的に証明する形式検証への招待
定理証明支援系 Isabelle/HOL チュートリアル
定理証明支援系 Coq チュートリアル
プログラム検証器を作って学ぶ Hoare 論理
Isabelle によるシーケント計算
関数型言語の操作的意味論 in Isabelle
もう1つの数学的帰納法と秘密の関数
代数的データ型のひみつを暴いて関数型プログラムを攻略する
余帰納法で無限リストを攻略する
等式論理と関数7個で作る証明検査器
プログラム検証と最弱事前条件のはなし
帰納的に定義された集合と最小不動点の密な関係
関数型言語の操作的意味論 in Isabelle
tackeさんからの挑戦状
プログラミング言語
“あとはゴミ集めだけ” Lisp キット
その他・一般
ソフトウェア開発を工学にする形式手法の紹介