自動検証 (ATVAの続き...)

自動検証って、出来る範囲は着実に広がっているんだけど... それは、ある意味で、コンピュータの能力が上がっているからなんだよな。結局、EXPTIME とかのアルゴリズムが多いし。変数の数を固定するとPTIMEとかって、ちょっと、ずるいと言えばずるい。

で、一方で、ソフトウェア/ハードウェアの複雑さはどんどん上がっているので、ぜんぜん、追い付いてません。

そのあたりのギャップがなぁ。でも、ある意味で、理論屋さんがどうこう言っても仕方のないところもある。ソフトウェア/ハードウェアを作る方が、結構、いい加減でも満足しているってことなのかも。

今日は、そういう風に感じる発表が多かったかな。