Loading user information from Channel 9

Something went wrong getting user information from Channel 9

Latest Achievement:

Loading user information from MSDN

Something went wrong getting user information from MSDN

Visual Studio Achievements

Latest Achievement:

Loading Visual Studio Achievements

Something went wrong getting the Visual Studio Achievements

Nikolaj Bjørner and Leonardo de Moura: The Z3 Constraint Solver

15 minutes, 29 seconds


Right click “Save as…”

Nikolaj Bjørner and Leonardo de Moura are Researchers in the Research in Software Engineering (RiSE) team at Microsoft Research. They are talking and demoing Z3, a high-performance SMT constraint solver. Solving constraint systems is the root of of many software analysis techniques so it is not surprising to see Z3 powering many tools developed at Microsoft: Spec#/Boogie, Pex, SLAM, SAGE, FORMULA, HAVOC and more.

In this video, you'll get a 10000 feet overview of Z3 and constraint solving in general with a demo on how to use the C# API. For more details, you will find many articles that should keep you busy for a while.

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.


Follow the discussion

  • Oops, something didn't work.

    Getting subscription
    Subscribe to this conversation
  • Very Cool

  • Aaron StainbackAceHack AceHack

    Great Stuff!  I plan on building a stable worm hole using Z3 and Infer.NET Smiley  Have a great new years.

  • Allan LindqvistaL_ Kinect ftw

    z3 is incredibly cool.. i didnt know there was a c# api though :O

    please, please make more z3 videos.. Smiley you could talk to bart de smet about his linq-to-z3 pet project



    the z3 release notes says the latest version is 2.4, but on the download page, only 2.3 is available

  • Tomasz Wisniewskiwisnia Tomasz Wisniewski

    Z3 i very cool! Too bad that the guys in this video are a litle bit camera shy and don't pass on their great knowledge as good as they could

  • Peli de Halleuxpeli Peli

    Hi Thomas,


    I already had to corner them in their offices to get the video Smiley I'll try to get more videos about the coolness of Z3.


    Cheers, Peli

  • Bent Rasmussenexoteric stuck in a loop, for a while

    Z3 is indeed very cool and it's great how it's becomming the one-stop shopping for SMT within the Microsoft tools ecosystem. It brings back memories of seeing PREfix and PREfast. I think this video is too short and stops quite abruptly which looked awkward to me. On the other hand I think the presentation itself was quite fine. Z3 and Microsoft Semantic Engine are two of the "top-most cool" technologies within Microsoft atm.

  • Michael A. VolzFlynn0r Passionate about code

    Nice videos with very interesting topics from you Peli. Thank´s a lot. Please keep it coming Wink

  • Nice video, one wish though -- could clip-in microphones can be used, because the volume level differs a lot from person to person.

  • Peli de Halleuxpeli Peli

    Good point. I've received my clip-on mics so things should work better for the next videos.

  • How does the performance of Z3 compare to, let's say, the CSP modules in Sicstus prolog?


  • HeleneHelene

    nice video:)

Remove this comment

Remove this thread


Comments closed

Comments have been closed since this content was published more than 30 days ago, but if you'd like to continue the conversation, please create a new thread in our Forums, or Contact Us and let us know.