<\/p>\n
Opens in a new tab<\/span><\/p>\n The Z3 Satisfiability Modulo Theories (SMT) problem solver is used in many different contexts. This meeting is an opportunity for researchers to exchange experiences with others and the developers of Z3. Participants are invited to present their applications and use of Z3. We will provide an update on new developments in Z3 as well as an assortment of social events.<\/p>\n We invite attendees to describe their uses of Z3. In particular we are interested to share experiences and to provide inspiration among users of Z3 and also extract useful challenges for Z3 and the SMT community. Describe your application. How does it invoke Z3? Which features are you using? What obstacles did you encounter? What alternatives have you considered and what are the trade-offs?<\/p>\n We will give a session on some of the newer features in Z3 as well as recurring themes. The topics include: Strategies, Model-based Quantifier instantiation (MBQI), Theory solvers, Real arithmetic solvers,\u00a0Proof objects, Simplification, Fixed-points, Configuring Z3, Quantifier instantiation with patterns, encoding techniques (e.g., bit-vectors or integers; using algebraic data-types and arrays).<\/p>\n<\/div>\n Opens in a new tab<\/span><\/p>\n The detailed program is to be determined. There will be three days of informal talks and social activities including dinners scheduled for the evenings.<\/p>\n We are happy to include two keynotes form Microsoft Researchers:<\/p>\n There will also be an interactive\u00a0session with several other Microsoft Research tools that use Z3.<\/p>\n<\/div>\n Opens in a new tab<\/span><\/p>\n A previous well attended Z3 SIG meeting was held in Cambridge, UK in 2011. View the program with slides<\/a>.<\/p>\n<\/div>\n Opens in a new tab<\/span><\/p>\n","protected":false},"excerpt":{"rendered":" This meeting is an opportunity for researchers to exchange experiences with others and the developers of Z3.<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr_startdate":"2012-10-22","msr_enddate":"2012-10-24","msr_location":"Microsoft Research, Redmond","msr_expirationdate":"","msr_event_recording_link":"","msr_event_link":"","msr_event_link_redirect":false,"msr_event_time":"","msr_hide_region":false,"msr_private_event":true,"msr_hide_image_in_river":0,"footnotes":""},"research-area":[13561],"msr-region":[197900],"msr-event-type":[197944],"msr-video-type":[],"msr-locale":[268875],"msr-program-audience":[],"msr-post-option":[],"msr-impact-theme":[],"class_list":["post-251324","msr-event","type-msr-event","status-publish","hentry","msr-research-area-algorithms","msr-region-north-america","msr-event-type-hosted-by-microsoft","msr-locale-en_us"],"msr_about":"\n\n <\/p>\n Opens in a new tab<\/span><\/p>\n The Z3 Satisfiability Modulo Theories (SMT) problem solver is used in many different contexts. This meeting is an opportunity for researchers to exchange experiences with others and the developers of Z3. Participants are invited to present their applications and use of Z3. We will provide an update on new developments in Z3 as well as an assortment of social events.<\/p>\n We invite attendees to describe their uses of Z3. In particular we are interested to share experiences and to provide inspiration among users of Z3 and also extract useful challenges for Z3 and the SMT community. Describe your application. How does it invoke Z3? Which features are you using? What obstacles did you encounter? What alternatives have you considered and what are the trade-offs?<\/p>\n We will give a session on some of the newer features in Z3 as well as recurring themes. The topics include: Strategies, Model-based Quantifier instantiation (MBQI), Theory solvers, Real arithmetic solvers,\u00a0Proof objects, Simplification, Fixed-points, Configuring Z3, Quantifier instantiation with patterns, encoding techniques (e.g., bit-vectors or integers; using algebraic data-types and arrays).<\/p>\n<\/div>\n Opens in a new tab<\/span><\/p>\n The detailed program is to be determined. There will be three days of informal talks and social activities including dinners scheduled for the evenings.<\/p>\n We are happy to include two keynotes form Microsoft Researchers:<\/p>\n There will also be an interactive\u00a0session with several other Microsoft Research tools that use Z3.<\/p>\n<\/div>\n Opens in a new tab<\/span><\/p>\n A previous well attended Z3 SIG meeting was held in Cambridge, UK in 2011. View the program with slides<\/a>.<\/p>\n<\/div>\n Opens in a new tab<\/span><\/p>\n","tab-content":[{"id":0,"name":"About","content":"Z3 in the Wild<\/h2>\n
Secret Sauce<\/h2>\n
\n
Z3 in the Wild<\/h2>\n
Secret Sauce<\/h2>\n
\n
Z3 in the Wild<\/h2>\r\nWe invite attendees to describe their uses of Z3. In particular we are interested to share experiences and to provide inspiration among users of Z3 and also extract useful challenges for Z3 and the SMT community. Describe your application. How does it invoke Z3? Which features are you using? What obstacles did you encounter? What alternatives have you considered and what are the trade-offs?\r\n
Secret Sauce<\/h2>\r\nWe will give a session on some of the newer features in Z3 as well as recurring themes. The topics include: Strategies, Model-based Quantifier instantiation (MBQI), Theory solvers, Real arithmetic solvers,\u00a0Proof objects, Simplification, Fixed-points, Configuring Z3, Quantifier instantiation with patterns, encoding techniques (e.g., bit-vectors or integers; using algebraic data-types and arrays).\r\n\r\n<\/div>\r\n
\r\n \t