"Verification Tool and Unified Specifications for Embedded Software"

業務論文です。pdf版はこちら。要旨は以下の通り。

In the extended abstract, our on-going research project Verification Tool and Unified Specifications for Embedded Software is explained. In the project, we are developing an upper-process support tool that helps ones formalize specifications of embedded software and verify a certain type of consistency and correctness unless formal method background is equipped. The tool is based on a proof assistant system (Agda) and a software development system (VDM tools), but is designed with the concept of lightweight formal methods. The project is being promoted as joint research with xxxxxxxxxxxxxxxx, under the program of the Ministry of xxxxxxxxxx.

Agdaでは「高階の対象を簡単に扱えるので仕様書の形式化が楽」と主張したら、N先生から「そんなに楽なら、証明課題の自動生成とか自動証明とかしてみたらどうだ（大意）」と質問されました（汗）。