PRINCIPIA
ProductsAbout Us

セミナー情報

形式手法に関するセミナーを開催しています.

詳細につきましては CONNPASS をご覧ください.

デッドロック発見器を作って学ぶマルチスレッドプログラミング

参加者が自分の好きなプログラミング言語でデッドロック発見器を作り,それを使ってマルチスレッドプログラミングを学ぶハンズオンセミナーです. 講師と対話しながら自らプログラムを書くことでマルチスレッドプログラミングを深く理解することができます.さらに作成したプログラムは設計分析ツールとして活用することができます.

共有変数編とメッセージ通信編の2つがあります.

モデル検査器を作って学ぶマルチスレッドプログラミング

「デッドロック発見器を作って学ぶマルチスレッドプログラミング ★共有変数編★」の続編です.

デッドロック発見器を拡張して,条件を見たす状態や実行パスを探索するモデル検査器を作ります.条件は計算木論理 (Computation Tree Logic, CTL) で指定します.自らプログラムを書くことでモデル検査のしくみを深く理解することができます.これにより強力な既存ツールを使いこなせるようになるでしょう.

SyncStitch: A Model Checker based on the Process Algebra CSP

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:

The behaviour of the system and the result of checking (violation or witness) can be shown as a computation tree and analyzed interactively.

News

14 June 2019 SyncStitch version 3 is released.