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

Play Nikolaj Bjørner and Leonardo de Moura: The Z3 Constraint Solver
Sign in to queue


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.



Right click to download this episode

The Discussion

  • User profile image

    Very Cool

  • User profile image

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

  • User profile image

    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

  • User profile image

    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

  • User profile image

    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

  • User profile image

    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.

  • User profile image

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

  • User profile image

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

  • User profile image

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

  • User profile image

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


  • User profile image

    nice video:)

Add Your 2 Cents