セミナー

現在予定されているセミナーにつきましては CONNPASS のページ をご覧ください．

セミナー開催のリクエストは isaac@principia-m.com までご連絡ください．

並行システム・プロセス代数 CSP・SyncStitch

• 並行システムの設計検証
• デッドロック発見器を作って学ぶマルチスレッドプログラミング ★共有変数編★
• デッドロック発見器を作って学ぶマルチスレッドプログラミング ★メッセージ通信編★
• CTL モデル検査器を作って学ぶマルチスレッドプログラミング
• LTL モデル検査器を作って学ぶマルチスレッドプログラミング
• トレース比較器を作って学ぶマルチスレッドプログラミング
• リファインメント検査器を作って学ぶマルチスレッドプログラミング
• アクターモデルに基づく並行合成器と分散システムの合意問題への適用例
• ロックフリーアルゴリズムのモデル化と分析
• プロセス代数 CSP 構文と操作的意味論
• 条件変数のモデル化と分析の例
• x86-TSO メモリモデルの分析

形式検証・定理証明・Isabelle・Coq

• プログラムの正しさを数学的に証明する形式検証への招待
• 定理証明支援系 Isabelle/HOL チュートリアル
• 定理証明支援系 Coq チュートリアル
• プログラム検証器を作って学ぶ Hoare 論理
• SMT solver によるテストケース生成器
• Isabelle によるシーケント計算
• 関数型言語の操作的意味論 in Isabelle
• もう1つの数学的帰納法と秘密の関数
• 代数的データ型のひみつを暴いて関数型プログラムを攻略する
• 余帰納法で無限リストを攻略する
• 等式論理と関数7個で作る証明検査器
• プログラム検証と最弱事前条件のはなし
• 帰納的に定義された集合と最小不動点の密な関係
• 関数型言語の操作的意味論 in Isabelle
• tackeさんからの挑戦状

プログラミング言語

• “あとはゴミ集めだけ” Lisp キット

その他・一般

• ソフトウェア開発を工学にする形式手法の紹介
• 振る舞い仕様の書きかた