証明の自動化の話

今更反応するのもどうかと思うのだが, リンクもトラックバックも無いので反応してないとも言う. 独り言.
どっかで聞いたなぁと思って色々考えてみたらUCとFormal methodだった. Dolev-Yao発祥のアレ.
ISEC 講演会「証明可能安全性の枠組」 岡本龍明（NTT）汎用的結合可能性（UC）について 発表資料 (pdf)の最後の方で触れられている. 日本応用数理学会と組んでやるそうですよ.