{"id":865743,"date":"2022-08-03T22:19:02","date_gmt":"2022-08-04T05:19:02","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-event&#038;p=865743"},"modified":"2022-08-17T06:28:26","modified_gmt":"2022-08-17T13:28:26","slug":"rise4fun-educational-workshop","status":"publish","type":"msr-event","link":"https:\/\/www.microsoft.com\/en-us\/research\/event\/rise4fun-educational-workshop\/","title":{"rendered":"Rise4Fun Educational Workshop"},"content":{"rendered":"\n\n\n\n\n<h2 id=\"logical-modeling-and-solving-with-z3\">Logical Modeling and Solving with Z3<\/h2>\n\n\n\n<p>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.&nbsp;<\/p>\n\n\n\n<p>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 <strong>no<\/strong> 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.&nbsp;<\/p>\n\n\n\n<h2 id=\"what-to-expect\">What to Expect<\/h2>\n\n\n\n<ul class=\"wp-block-list\"><li>A fun online Z3 learning session using a web-based tutorial, interleaving with interactions with authors of the tutorial as well as other learners;&nbsp;<ul><li>Software requirements: Chrome >=52.0, Edge >=16.0, Safari >= 11.0, or Firefox >= 53.0. For other browsers, see details <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/caniuse.com\/wasm\" target=\"_blank\" rel=\"noreferrer noopener\">here<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.&nbsp;<\/li><\/ul><\/li><li>An opportunity post-workshop to share your feedback on the workshop and the tutorial through questionnaires.&nbsp;<\/li><\/ul>\n\n\n\n<h2 id=\"speakers-ruanqianqian-lisa-huang-ayana-monroe-and-nikolaj-bjorner\">Speakers: Ruanqianqian (Lisa) Huang, Ayana&nbsp;Monroe and Nikolaj Bj\u00f8rner<\/h2>\n\n\n\n<p>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.&nbsp;We currently have a version of rise4fun instantiated to z3. It is available from <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/microsoft.github.io\/z3guide\">https:\/\/microsoft.github.io\/z3guide<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>&nbsp;&nbsp;<\/p>\n\n\n\n<h2 id=\"schedule\">Schedule<\/h2>\n\n\n\n<figure class=\"wp-block-table is-style-stripes\"><table><thead><tr><th>Time<\/th><th>Session<\/th><\/tr><\/thead><tbody><tr><td>9:00 AM\u201310:20 AM<\/td><td>Part I<\/td><\/tr><tr><td>10:20 AM\u201310:30 AM<\/td><td>Break<\/td><\/tr><tr><td>10:30 AM\u201311:45 AM<\/td><td>Part II<\/td><\/tr><tr><td>11:45 AM\u201312:00 PM<\/td><td>Wrap up, post-workshop questionnaire<\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n<div style=\"height:25px\" aria-hidden=\"true\" class=\"wp-block-spacer\"><\/div>\n\n\n\n<h2 id=\"registration\">Registration<\/h2>\n\n\n\n<p>To attend, we ask that you agree to participate in our study by signing the consent form found here<\/p>\n\n\n\n<div class=\"wp-block-buttons is-layout-flex wp-block-buttons-is-layout-flex\">\n<div class=\"wp-block-button is-style-fill\"><a data-bi-type=\"button\" class=\"wp-block-button__link\" href=\"https:\/\/teams.microsoft.com\/registration\/v4j5cvGGr0GRqy180BHbRw,j_z7oymuSUate1IcsUUqeA,PQU2lixpskCSAJJWU1m78w,k4h0jMLwNESMt5sIE7WBaw,RW48YEbqs0qLMKKgXz9Kfg,UiegadjHXUasNcxfASeAQg?mode=read&tenantId=72f988bf-86f1-41af-91ab-2d7cd011db47\" target=\"_blank\" rel=\"noreferrer noopener\">Participate in the study<\/a><\/div>\n<\/div>\n\n\n\n<hr class=\"wp-block-separator has-alpha-channel-opacity is-style-dots\"\/>\n\n\n\n<div style=\"height:10px\" aria-hidden=\"true\" class=\"wp-block-spacer\"><\/div>\n\n\n\n<h3 id=\"microsofts-event-code-of-conduct\">Microsoft\u2019s Event Code of Conduct<\/h3>\n\n\n\n<p>Microsoft\u2019s 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.<\/p>\n\n\n\n<p>We do not tolerate any behavior that is degrading to any gender, race, sexual orientation or disability, or any behavior that would violate <a href=\"https:\/\/www.microsoft.com\/en-us\/legal\/compliance\/default.aspx\">Microsoft\u2019s Anti-Harassment and Anti-Discrimination Policy, Equal Employment Opportunity Policy, or Standards of Business Conduct<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>. In short, the entire experience must meet our culture standards. We encourage everyone to assist in creating a welcoming and safe environment. Please <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/app.convercent.com\/en-us\/Anonymous\/IssueIntake\/LandingPage\/65d3b907-0933-e611-8105-000d3ab03673\" target=\"_blank\" rel=\"noreferrer noopener\">report<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> 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.<\/p>\n\n\n\n<div class=\"wp-block-buttons is-layout-flex wp-block-buttons-is-layout-flex\">\n<div class=\"wp-block-button is-style-outline is-style-outline--2378890ab75cce947d0f7e938a34b4a5\"><a data-bi-type=\"button\" class=\"wp-block-button__link\" href=\"https:\/\/aka.ms\/reportconcern\" target=\"_blank\" rel=\"noreferrer noopener\">Report a concern<\/a><\/div>\n<\/div>\n\n\n","protected":false},"excerpt":{"rendered":"<p>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 [&hellip;]<\/p>\n","protected":false},"featured_media":865869,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_startdate":"2022-08-24","msr_enddate":"2022-08-24","msr_location":"Virtual","msr_expirationdate":"","msr_event_recording_link":"","msr_event_link":"","msr_event_link_redirect":false,"msr_event_time":"9:00 AM\u201312:00 PM (PST)","msr_hide_region":false,"msr_private_event":false,"footnotes":""},"research-area":[13560],"msr-region":[256048],"msr-event-type":[197944],"msr-video-type":[],"msr-locale":[268875],"msr-program-audience":[],"msr-post-option":[],"msr-impact-theme":[],"class_list":["post-865743","msr-event","type-msr-event","status-publish","has-post-thumbnail","hentry","msr-research-area-programming-languages-software-engineering","msr-region-global","msr-event-type-hosted-by-microsoft","msr-locale-en_us"],"msr_about":"<!-- wp:msr\/event-details {\"title\":\"Rise4Fun Educational Workshop\",\"image\":{\"id\":865869,\"url\":\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2022\/07\/Z3-logo_banner_v2.jpg\",\"alt\":\"Z3 logo on grey background\"},\"backgroundColor\":\"purple\"} \/-->\n\n<!-- wp:msr\/content-tabs -->\n<!-- wp:msr\/content-tab -->\n<!-- wp:heading -->\n<h2>Logical Modeling and Solving with Z3<\/h2>\n<!-- \/wp:heading -->\n\n<!-- wp:paragraph -->\n<p>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.&nbsp;<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:paragraph -->\n<p>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 <strong>no<\/strong> 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.&nbsp;<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:heading -->\n<h2>What to Expect<\/h2>\n<!-- \/wp:heading -->\n\n<!-- wp:list -->\n<ul><li>A fun online Z3 learning session using a web-based tutorial, interleaving with interactions with authors of the tutorial as well as other learners;&nbsp;<ul><li>Software requirements: Chrome &gt;=52.0, Edge &gt;=16.0, Safari &gt;= 11.0, or Firefox &gt;= 53.0. For other browsers, see details <a href=\"https:\/\/caniuse.com\/wasm\" target=\"_blank\" rel=\"noreferrer noopener\">here<\/a>.&nbsp;<\/li><\/ul><\/li><li>An opportunity post-workshop to share your feedback on the workshop and the tutorial through questionnaires.&nbsp;<\/li><\/ul>\n<!-- \/wp:list -->\n\n<!-- wp:heading -->\n<h2>Speakers: Ruanqianqian (Lisa) Huang, Ayana&nbsp;Monroe and Nikolaj Bj\u00f8rner<\/h2>\n<!-- \/wp:heading -->\n\n<!-- wp:paragraph -->\n<p>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.&nbsp;We currently have a version of rise4fun instantiated to z3. It is available from <a href=\"https:\/\/microsoft.github.io\/z3guide\">https:\/\/microsoft.github.io\/z3guide<\/a>&nbsp;&nbsp;<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:heading -->\n<h2>Schedule<\/h2>\n<!-- \/wp:heading -->\n\n<!-- wp:table {\"className\":\"is-style-stripes\"} -->\n<figure class=\"wp-block-table is-style-stripes\"><table><thead><tr><th>Time<\/th><th>Session<\/th><\/tr><\/thead><tbody><tr><td>9:00 AM\u201310:20 AM<\/td><td>Part I<\/td><\/tr><tr><td>10:20 AM\u201310:30 AM<\/td><td>Break<\/td><\/tr><tr><td>10:30 AM\u201311:45 AM<\/td><td>Part II<\/td><\/tr><tr><td>11:45 AM\u201312:00 PM<\/td><td>Wrap up, post-workshop questionnaire<\/td><\/tr><\/tbody><\/table><\/figure>\n<!-- \/wp:table -->\n\n<!-- wp:spacer {\"height\":\"25px\"} -->\n<div style=\"height:25px\" aria-hidden=\"true\" class=\"wp-block-spacer\"><\/div>\n<!-- \/wp:spacer -->\n\n<!-- wp:heading -->\n<h2>Registration<\/h2>\n<!-- \/wp:heading -->\n\n<!-- wp:paragraph -->\n<p>To attend, we ask that you agree to participate in our study by signing the consent form found here<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:buttons -->\n<div class=\"wp-block-buttons\"><!-- wp:button {\"className\":\"is-style-fill\"} -->\n<div class=\"wp-block-button is-style-fill\"><a class=\"wp-block-button__link\" href=\"https:\/\/teams.microsoft.com\/registration\/v4j5cvGGr0GRqy180BHbRw,j_z7oymuSUate1IcsUUqeA,PQU2lixpskCSAJJWU1m78w,k4h0jMLwNESMt5sIE7WBaw,RW48YEbqs0qLMKKgXz9Kfg,UiegadjHXUasNcxfASeAQg?mode=read&amp;tenantId=72f988bf-86f1-41af-91ab-2d7cd011db47\" target=\"_blank\" rel=\"noreferrer noopener\">Participate in the study<\/a><\/div>\n<!-- \/wp:button --><\/div>\n<!-- \/wp:buttons -->\n\n<!-- wp:separator {\"className\":\"is-style-dots\"} -->\n<hr class=\"wp-block-separator has-alpha-channel-opacity is-style-dots\"\/>\n<!-- \/wp:separator -->\n\n<!-- wp:spacer {\"height\":\"10px\"} -->\n<div style=\"height:10px\" aria-hidden=\"true\" class=\"wp-block-spacer\"><\/div>\n<!-- \/wp:spacer -->\n\n<!-- wp:heading {\"level\":3} -->\n<h3>Microsoft\u2019s Event Code of Conduct<\/h3>\n<!-- \/wp:heading -->\n\n<!-- wp:paragraph -->\n<p>Microsoft\u2019s 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.<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:paragraph -->\n<p>We do not tolerate any behavior that is degrading to any gender, race, sexual orientation or disability, or any behavior that would violate <a href=\"https:\/\/www.microsoft.com\/en-us\/legal\/compliance\/default.aspx\">Microsoft\u2019s Anti-Harassment and Anti-Discrimination Policy, Equal Employment Opportunity Policy, or Standards of Business Conduct<\/a>. In short, the entire experience must meet our culture standards. We encourage everyone to assist in creating a welcoming and safe environment. Please <a href=\"https:\/\/app.convercent.com\/en-us\/Anonymous\/IssueIntake\/LandingPage\/65d3b907-0933-e611-8105-000d3ab03673\" target=\"_blank\" rel=\"noreferrer noopener\">report<\/a> 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.<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:buttons -->\n<div class=\"wp-block-buttons\"><!-- wp:button {\"className\":\"is-style-outline\"} -->\n<div class=\"wp-block-button is-style-outline\"><a class=\"wp-block-button__link\" href=\"https:\/\/aka.ms\/reportconcern\" target=\"_blank\" rel=\"noreferrer noopener\">Report a concern<\/a><\/div>\n<!-- \/wp:button --><\/div>\n<!-- \/wp:buttons -->\n<!-- \/wp:msr\/content-tab -->\n<!-- \/wp:msr\/content-tabs -->","tab-content":[],"msr_startdate":"2022-08-24","msr_enddate":"2022-08-24","msr_event_time":"9:00 AM\u201312:00 PM (PST)","msr_location":"Virtual","msr_event_link":"","msr_event_recording_link":"","msr_startdate_formatted":"August 24, 2022","msr_register_text":"Watch now","msr_cta_link":"","msr_cta_text":"","msr_cta_bi_name":"","featured_image_thumbnail":"<img width=\"960\" height=\"540\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2022\/07\/Z3-logo_banner_v2-960x540.jpg\" class=\"img-object-cover\" alt=\"Z3 logo on grey background\" decoding=\"async\" loading=\"lazy\" srcset=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2022\/07\/Z3-logo_banner_v2-960x540.jpg 960w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2022\/07\/Z3-logo_banner_v2-1066x600.jpg 1066w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2022\/07\/Z3-logo_banner_v2-655x368.jpg 655w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2022\/07\/Z3-logo_banner_v2-343x193.jpg 343w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2022\/07\/Z3-logo_banner_v2-640x360.jpg 640w, https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2022\/07\/Z3-logo_banner_v2-1280x720.jpg 1280w\" sizes=\"(max-width: 960px) 100vw, 960px\" \/>","event_excerpt":"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.&nbsp; In this workshop, we will provide an introduction to Z3, and how&hellip;","msr_research_lab":[],"related-researchers":[{"type":"user_nicename","display_name":"Nikolaj Bj\u00f8rner","user_id":33067,"people_section":"Section name 0","alias":"nbjorner"}],"msr_impact_theme":[],"related-academic-programs":[],"related-groups":[],"related-projects":[825511],"related-opportunities":[],"related-publications":[],"related-videos":[],"related-posts":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/865743"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-event"}],"version-history":[{"count":23,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/865743\/revisions"}],"predecessor-version":[{"id":873456,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/865743\/revisions\/873456"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/865869"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=865743"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=865743"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=865743"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=865743"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=865743"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=865743"},{"taxonomy":"msr-program-audience","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-program-audience?post=865743"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=865743"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=865743"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}