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

Posted By: Peli de Halleux | Dec 31st, 2009 @ 11:00 AM | 46,983 Views | 9 Comments
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.
Rating:
6
0
#Dec 31st, 2009 @ 5:22 PM
AceHack
AceHack
AceHack

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

#Jan 1st @ 5:45 AM
aL_
aL_
Rx 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

 

btw,

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

#Jan 1st @ 8:40 AM
wisnia
wisnia
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

#Jan 1st @ 9:26 AM
peli
peli
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

#Jan 1st @ 9:28 AM
exoteric
exoteric
embarassingly sequential

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.

#Jan 1st @ 10:09 AM
Flynn0r
Flynn0r
Passionate about code

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

#Jan 5th @ 3:25 AM
macias
macias

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

#Jan 5th @ 11:39 AM
peli
peli
Peli

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

Microsoft Communities