InfoQ ホームページ Z3 に関するすべてのコンテンツ
ニュース
RSSフィード-
Microsoft，タイプセーフなオペレーティングシステム Verve を発表
Microsoft Research は Singularity プロジェクトから派生したオペレーティングシステムである Verve のリリースを発表した。TAL (Typed Assembly Language，型付きアセンブリ言語) と Hoare 論理の採用を前提とすることで，最高レベルのセキュリティと安全性を実現する。
-
LINQ to Z3、世界最速の定理証明器
マイクロソフトリサーチは、Z3は、世界最速の定理証明器であると宣言した。Z3は、ほかのアプリケーションへの低レベルツールとして設計されており、単独では動作しない。定理証明器のホストは、 Spec#/Boogie、Pex、Yogi、Vigilante、SLAM、F7、SAGE、VS3、FORMULA、HAVOCを含む数多のプロジェクトで使用されている。Bart De Smet氏のLINQ to Z3を使えば、驚くほど簡単に使えるようになる。