BT

Facilitating the Spread of Knowledge and Innovation in Professional Software Development

Write for InfoQ

Topics

Choose your language

InfoQ Homepage Z3 Content on InfoQ

News

RSS Feed
  • Announcing Verve – A Type-Safe Operating System

    Microsoft Research releases Verve, an operating system which grew out of the Singularity project, upon whose base premise is to use Typed Assembly Language, TAL, and Hoare logic to achieve the highest levels of security and safety.

  • LINQ to Z3, The World’s Fasted Theorem Prover

    Microsoft Research claims that Z3 is the world’s fastest theorem prover. Z3 is designed to be a low-level tool for other applications, it is not meant to stand-alone. With its host of theorem provers, it is used by numerous projects including Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC. With Bart De Smet’s LINQ to Z3, using this tool becomes embarrassingly easy.

BT