量子コンピュータとモデル検査

こんにちは。株式会社フォーマルテックの早水です。

夕方のテレビのニュース番組を見ていて、とてもうれしいニュースが飛び込んできました。国立情報学研究所が国産量子コンピュータを開発し、無償公開するというのです。インターネットのニュースサイトでも記事が出ています。

記事

なぜ、うれしいかと言うと？私の夢の1つに「いつか量子コンピュータ上でモデル検査をしてみたい！」というのがあるからです。

記事によると、試作機の段階でスパコンの100倍の速度で演算でき、今後も性能向上を目指すそうです。これまで、状態爆発が発生して検査できなかった事例や、数万行のソースコードのモデル検査を実現できるかもしれないと考えると、心がワクワクしてきます。

11/27から一般公開され、申請すれば利用できるそうです。残念ながら、現時点ではまだ、モデル検査ツールは動かせないみたいですが、近い？or 遠い？将来、OSを搭載した汎用機が登場すれば、是非、モデル検査を実行してみたいと思います。