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

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

前回の投稿で紹介した量子コンピュータの利用サイトが公開されたようです。以下のサイトです。

Quantum Neural Network

んー、覚悟はしていましたが、やはり英語のサイトです・・・。世界中の研究者に公開するとのことなので当然ですね。アカウントの作成だけはできそうですが、量子コンピュータの仕組みと利用方法が分からないので「冷やかし」は控えたいと思います。

懇意にして頂いている某研究所の研究者の方が「使ってみて結果が得られたら情報共有します」とおっしゃってくれているので、それを待つことにします。もし、モデル検査が実現すれば大変な朗報です。

本記事のさらに続編を公開できる日が来ることを期待しています。

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

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

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

記事

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

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

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

モデル検査の情報交換会

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

今日(2017/11/17)は、モデル検査についての情報交換会(単なる飲み会ですが・・・)に参加してきます。お相手は某大手メーカの方たちです。モデル検査ツールSPINを使われていて、職場でモデル検査を広めようと頑張っていらっしゃいます。

モデル検査について大いに盛り上がりたいと思います。

ウインターワークショップ2018に参加しませんか?

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

ウインターワークショップ2018・イン・宮島に参加しませんか?

このワークショップでは、2012年より岡山県立大学の横川先生と共同で毎年、形式手法セッションを開催して、二人で討論リーダを務めております。形式手法は回路設計などのハードウェア分野では定番の技術として、しっかり定着しているようですが、ソフトウェアの分野では広く普及しているとは言い難い状況です。横川先生とは形式手法に対する強い思いに、お互いに共感し合って、モデル検査を含む形式手法の普及拡大を目指しております。セッションの詳細は以下をご覧ください。

T4: 形式手法-導入支援と技術教育-

参加区分は以下の3つです。

ポジションペーパー(論文)/プレゼンテーションのみ/議論への参加のみ

論文の投稿や発表がなくても、「議論への参加のみ」の区分を選択すれば参加できます。同セッションでは、正式な学会のような研究発表も歓迎ですし、ちょっとした提案、日頃疑問に思うこと、問題の共有など、ざっくばらんに議論できればと思っております。

初日(2018/1/18)の夜には情報交換会が開催されますので、広島の美味しい「牡蠣」を頂きながら、楽しくお話をしましょう。

ビジネス・エンカレッジ・フェアに参加しました。

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

先週の木曜日(11/9)に、ビジネス・エンカレッジ・フェア2017(池田泉州銀行主催)に参加してきました。業務で懇意にして頂いているプロアシストさんが出展されているとのことで、ブースを訪問しました。

写真はプロアシストさんのブースと知り合いのHさんです。Hさんが横になっているのは、緊張を解きほぐすロッキングチェアだそうで、北欧では相応の市場規模があるそうです。

私も横になってみましたが、開始するとゆっくりと揺れて、音楽が流れてきます。本来は介護施設等で緊張をほぐすのが目的だそうですが、就寝前に30分ほど使うと良い「ナイトキャップ」になると思いました。