Nikolaj Bjørner and Leonardo de Moura: The Z3 Constraint Solver
- Posted: Dec 31, 2009 at 11:00 AM
- 54,060 Views
- 11 Comments
Download
How do I download the videos?
- To download, right click the file type you would like and pick “Save target as…” or “Save link as…”
Why should I download videos from Channel9?
- It's an easy way to save the videos you like locally.
- You can save the videos in order to watch them offline.
- If all you want is to hear the audio, you can download the MP3!
Which version should I choose?
- If you want to view the video on your PC, Xbox or Media Center, download the High Quality WMV file (this is the highest quality version we have available).
- If you'd like a lower bitrate version, to reduce the download time or cost, then choose the Medium Quality WMV file.
- If you have a Zune, WP7, iPhone, iPad, or iPod device, choose the low or medium MP4 file.
- If you just want to hear the audio of the video, choose the MP3 file.
Right click “Save as…”
- MP3 (Audio only)
- MP4 (iPod, Zune HD)
- Mid Quality WMV (Lo-band, Mobile)
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.
- Try Z3 in your web browser at http://rise4fun.com/z3!
- Z3 home page
The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.
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.
Follow the Discussion
Very Cool
Great Stuff! I plan on building a stable worm hole using Z3 and Infer.NET
Have a great new years.
z3 is incredibly cool.. i didnt know there was a c# api though :O
please, please make more z3 videos..
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
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
Hi Thomas,
I already had to corner them in their offices to get the video
I'll try to get more videos about the coolness of Z3.
Cheers, Peli
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.
Nice videos with very interesting topics from you Peli. Thank´s a lot. Please keep it coming
Nice video, one wish though -- could clip-in microphones can be used, because the volume level differs a lot from person to person.
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?
thanks
nice video:)
Remove this comment
Remove this thread
close