Peli at RiSE

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

Download this episode

Download Video

Description

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.

Embed

Format

Available formats for this video:

Actual format may change based on video formats available and browser capability.

    The Discussion

    • scientist

      Very Cool

    • AceHack

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

    • aL_

      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

       

      btw,

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

    • wisnia

      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

      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

    • exoteric

      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.

    • Flynn0r

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

    • macias

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

    • peli

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

    • thelazydogs​back

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

      thanks

    • Helene

      nice video:)

    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.