InfoQ ホームページ Theorem-Prover に関するすべてのコンテンツ
ニュース
RSSフィード-
Idrisが間もなくバージョン1.0に
依存型(dependent type)ベース言語のIdrisが間もなくバージョン0.99に到達する。Idrisチームによると，1.00のアルファ版として見ることができるものだ。Idris 1.0のリリースは2017年2月頃と予想される。
-
LINQ to Z3、世界最速の定理証明器
マイクロソフトリサーチは、Z3は、世界最速の定理証明器であると宣言した。Z3は、ほかのアプリケーションへの低レベルツールとして設計されており、単独では動作しない。定理証明器のホストは、 Spec#/Boogie、Pex、Yogi、Vigilante、SLAM、F7、SAGE、VS3、FORMULA、HAVOCを含む数多のプロジェクトで使用されている。Bart De Smet氏のLINQ to Z3を使えば、驚くほど簡単に使えるようになる。