Microsoft Research DownloadsKeep current with all the latest Microsoft Research DownloadsZ3- June 19, 2008 Z3 is an SMT solver that combines several theory solvers into a combined framework. It can be used to prove theorems and find counter-examples for non-theorems.http://research.microsoft.com/research/downloads/rss_redirect.aspx?0rc=d&id=1286 Random-Access Vector Graphics- June 13, 2008 This program demonstrates our work on random-access rendering anti-aliased vector graphics on the GPU. We support a broad class of vector primitives, including multiple layers of semitransparent fills and strokes, with quadratic outlines and color gradients. Our approach is to create a coarse lattice in which each cell contains a variable-length encoding of the graphics primitives that overlap it. These cell-specialized encodings are interpreted at run time within a pixel shader. Advantages...http://research.microsoft.com/research/downloads/rss_redirect.aspx?0rc=d&id=1278 HAVOC: Heap-Aware Verifier for C Programs- June 3, 2008 HAVOC is a modular verifier for systems software written in C. It takes as input an annotated C program, in the form of pre- and post-conditions and loop invariants, and uses the Boogie verifier and the SMT solver Z3 to check the annotations. The novelty of the tool lies in a) an accurate memory model for C accounting for low-level operations such as pointer arithmetic, address-of operations, and casts; b) an expressive annotation language; and c) efficient decision procedures to reason about...http://research.microsoft.com/research/downloads/rss_redirect.aspx?0rc=d&id=1275 |