Rise4Fun Educational Workshop

Logical Modeling and Solving with Z3

Are you curious about logical reasoning in Computer Science? Have you thought about incorporating logical reasoning into your new or ongoing projects, not knowing where to start or having a global overview? Come learn how to use Z3! Z3 is a state-of-the-art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas. It supports optimized theory reasoning. 

In this workshop, we will provide an introduction to Z3, and how to use Z3 effectively for logical modeling and solving. Participants will learn to master Z3 in the SMT-LIB2 format and using scripts by following an online Z3 guide we have developed. The tutorial requires no local installation of Z3. This workshop targets those who want to equip themselves with the basics of Z3 to prepare for coursework, research and ongoing projects. All levels of experience with programming and/or logical reasoning are welcomed. 

What to Expect

• A fun online Z3 learning session using a web-based tutorial, interleaving with interactions with authors of the tutorial as well as other learners; 
  • Software requirements: Chrome >=52.0, Edge >=16.0, Safari >= 11.0, or Firefox >= 53.0. For other browsers, see details here (opens in new tab). 
• An opportunity post-workshop to share your feedback on the workshop and the tutorial through questionnaires. 

Speakers: Ruanqianqian (Lisa) Huang, Ayana Monroe and Nikolaj Bjørner

Microsoft Research and the rise4fun team have launched a new and improved version of the rise4fun tool. The goal of the tool is to generate a platform with additional educational content that is successful in supporting educators and students alike. We currently have a version of rise4fun instantiated to z3. It is available from https://microsoft.github.io/z3guide (opens in new tab)  

Schedule

Registration

To attend, we ask that you agree to participate in our study by signing the consent form found here

Microsoft’s Event Code of Conduct

Microsoft’s mission is to empower every person and every organization on the planet to achieve more. This includes virtual events Microsoft hosts and participates in, where we seek to create a respectful, friendly, and inclusive experience for all participants. As such, we do not tolerate harassing or disrespectful behavior, messages, images, or interactions by any event participant, in any form, at any aspect of the program including business and social activities, regardless of location.

We do not tolerate any behavior that is degrading to any gender, race, sexual orientation or disability, or any behavior that would violate Microsoft’s Anti-Harassment and Anti-Discrimination Policy, Equal Employment Opportunity Policy, or Standards of Business Conduct (opens in new tab). In short, the entire experience must meet our culture standards. We encourage everyone to assist in creating a welcoming and safe environment. Please report (opens in new tab) any concerns, harassing behavior, or suspicious or disruptive activity. Microsoft reserves the right to ask attendees to leave at any time at its sole discretion.