新製品ニュース〜モデル・チェッキング用のフォーマル・ベリファイア，　汎用と特定用途向けを用意
日経エレクトロニクス　第743号　1999.5.17

　米Ｃｈｒｙｓａｌｉｓ　Ｓｙｍｂｏｌｉｃ　Ｄｅｓｉｇｎ，Ｉｎｃ．は，モデル・チェッキング用のフォーマル・ベリファイアを複数発売する。モデル・チェッキング用のフォーマル・ベリファイアは，設計結果が設計仕様（プロパティ）に沿っているかどうかを解析するためのツールで，プロパティ・チェッカとも呼ばれる。数学的に解析するため，シミュレーションのようなテスト・ベクトルが不要なうえ，原理的には検証の漏れがない。…