{"id":251948,"date":"2016-07-11T10:37:22","date_gmt":"2016-07-11T17:37:22","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-event&p=251948"},"modified":"2022-08-31T13:32:34","modified_gmt":"2022-08-31T20:32:34","slug":"z3-special-interest-group-2011","status":"publish","type":"msr-event","link":"https:\/\/www.microsoft.com\/en-us\/research\/event\/z3-special-interest-group-2011\/","title":{"rendered":"Z3 Special Interest Group 2011"},"content":{"rendered":"\n\n\n\n\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

\n

Z3 in the Wild<\/h2>\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

Secret Sauce<\/h2>\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, Proof 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\n\n\n\n\n

There will be three days of informal talks and social activities including dinners scheduled for the evenings.<\/p>\n

PDF version of the program<\/a>.<\/p>\n

Wednesday, November 2<\/h3>\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n
9.00<\/td>\nWelcome & Breakfast<\/td>\n<\/tr>\n
9.30<\/td>\nTony Hoare<\/strong><\/td>\n<\/tr>\n
<\/td>\nThe Verified Software Initiative<\/td>\n<\/tr>\n
<\/td>\nHillel Kugler<\/strong><\/td>\n<\/tr>\n
<\/td>\nZ3 for Biology<\/td>\n<\/tr>\n
10.30<\/td>\nBreak<\/td>\n<\/tr>\n
11.00<\/td>\nThe Z3 Team<\/strong><\/td>\n<\/tr>\n
<\/td>\nNew and future features of Z3 Slides 1<\/a> Slides 2<\/a><\/td>\n<\/tr>\n
12.00<\/td>\nLunch<\/td>\n<\/tr>\n
13.30<\/td>\nAdrien Champion<\/strong><\/td>\n<\/tr>\n
<\/td>\nAssumptio and Stuff: using Z3 in a collaborative parallel formal verification framework. Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nMarko K\u00e4\u00e4ramees<\/strong><\/td>\n<\/tr>\n
<\/td>\nSymbolic analysis of EFSM models for test generation using Z3 Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nJuhan Ernits<\/strong><\/td>\n<\/tr>\n
<\/td>\nApplication of Z3 in Consistency Based Diagnosis of Hybrid Systems and Beyond<\/td>\n<\/tr>\n
15.00<\/td>\nBreak<\/td>\n<\/tr>\n
15.30<\/td>\nMalte Schwerhoff<\/strong><\/td>\n<\/tr>\n
<\/td>\nComparing Verification Condition Generation with Symbolic Execution Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nJoseph N. Ruskiewicz<\/strong><\/td>\n<\/tr>\n
<\/td>\nUsing Debuggers to Understand Failed Verification Attempts<\/td>\n<\/tr>\n
<\/td>\nArlen Cox<\/strong><\/td>\n<\/tr>\n
<\/td>\nCounterexample Generation for Separation Logic Slides<\/a><\/td>\n<\/tr>\n
17.00<\/td>\nClose<\/td>\n<\/tr>\n
18.00<\/td>\nCoach to pick up attendees from MSRC<\/td>\n<\/tr>\n
19.00<\/td>\nEvening Dinner at Restaurant Alimentum<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

 <\/p>\n

Thursday, November 3<\/h3>\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n
9.00<\/td>\nWelcome & Breakfast<\/td>\n<\/tr>\n
9.30<\/td>\nByron Cook<\/strong><\/td>\n<\/tr>\n
<\/td>\nSymbolic software model checking with Z3<\/td>\n<\/tr>\n
<\/td>\nAndrey Rybalchenko<\/strong><\/td>\n<\/tr>\n
<\/td>\nTowards Automatic Synthesis of Software Verification Tools<\/td>\n<\/tr>\n
10.30<\/td>\nBreak<\/td>\n<\/tr>\n
11.00<\/td>\nNik Sultana<\/strong><\/td>\n<\/tr>\n
<\/td>\nSolving trust issues using Z3 Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nAlexander Malkis<\/strong><\/td>\n<\/tr>\n
<\/td>\nAutomatic verification of software barriers: Z3 vs. MONA vs. BAPA.<\/td>\n<\/tr>\n
12.00<\/td>\nLunch<\/td>\n<\/tr>\n
13.30<\/td>\nChantal Keller<\/strong><\/td>\n<\/tr>\n
<\/td>\nCertification of SMT proof witnesses in the Coq proof assistant Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nTjark Weber<\/strong><\/td>\n<\/tr>\n
<\/td>\nIndependent Proof Reconstruction for Z3: An Overview<\/td>\n<\/tr>\n
<\/td>\nSascha Boehme<\/strong><\/td>\n<\/tr>\n
<\/td>\nProof Automation for Isabelle via Z3<\/td>\n<\/tr>\n
15.00<\/td>\nBreak<\/td>\n<\/tr>\n
15.30<\/td>\nJasmin Blanchette<\/strong><\/td>\n<\/tr>\n
<\/td>\nSledgehammer with Z3 Makes Isabelle Happy<\/td>\n<\/tr>\n
<\/td>\nKonstantin Korovin and Christoph Sticksel<\/strong><\/td>\n<\/tr>\n
<\/td>\nZ3 for iProver-Eq: efficient ground solving for instantiation-based first-order reasoning Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nPhilippe Suter<\/strong><\/td>\n<\/tr>\n
<\/td>\nProgramming with Z3<\/td>\n<\/tr>\n
17.00<\/td>\nClose<\/td>\n<\/tr>\n
19.00<\/td>\nEvening Dinner at Corpus Christi College<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

Friday, November 4<\/h3>\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n
9.00<\/td>\nWelcome & Breakfast<\/td>\n<\/tr>\n
9.30<\/td>\nCarsten Fuhs<\/strong><\/td>\n<\/tr>\n
<\/td>\nAutomated Termination Analysis for Programming Languages via Non-Linear SMT and Term Rewriting<\/td>\n<\/tr>\n
<\/td>\nSilvio Ranise<\/strong><\/td>\n<\/tr>\n
<\/td>\nSymbolic Backward Reachability with Effectively Propositional Logic<\/td>\n<\/tr>\n
10.30<\/td>\nBreak<\/td>\n<\/tr>\n
11.00<\/td>\nPaul Jackson<\/strong><\/td>\n<\/tr>\n
<\/td>\nProving SPARK-Ada verification conditions using SMT solvers<\/td>\n<\/tr>\n
<\/td>\nMargus Veanes<\/strong><\/td>\n<\/tr>\n
<\/td>\nMicrosoft.Automata library: application to Bek<\/td>\n<\/tr>\n
12.00<\/td>\nLunch<\/td>\n<\/tr>\n
13.30<\/td>\nSwen Jacobs<\/strong><\/td>\n<\/tr>\n
<\/td>\nSMT-based Reactive Synthesis<\/td>\n<\/tr>\n
<\/td>\nMarek Trtik<\/strong><\/td>\n<\/tr>\n
<\/td>\nOverapproximating Program Paths using FOL Formula Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nMaria Paola Bonacina<\/strong><\/td>\n<\/tr>\n
<\/td>\nTowards an interpolating DPLL(Gamma+T) Slides<\/a><\/td>\n<\/tr>\n
15.00<\/td>\nBreak<\/td>\n<\/tr>\n
15.30<\/td>\nVladimir Klebanov<\/strong><\/td>\n<\/tr>\n
<\/td>\nTheory reasoning in deductive program verification Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nDenis Nicole<\/strong><\/td>\n<\/tr>\n
<\/td>\nThe ESBMC model checker for multi-threaded C<\/td>\n<\/tr>\n
17.00<\/td>\nClose<\/td>\n<\/tr>\n
19.00<\/td>\nPub crawl<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n\n\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":"2011-11-02","msr_enddate":"2011-11-04","msr_location":"Microsoft Research, Cambridge","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":[239178],"msr-event-type":[197944],"msr-video-type":[],"msr-locale":[268875],"msr-program-audience":[],"msr-post-option":[],"msr-impact-theme":[],"class_list":["post-251948","msr-event","type-msr-event","status-publish","hentry","msr-research-area-algorithms","msr-region-europe","msr-event-type-hosted-by-microsoft","msr-locale-en_us"],"msr_about":"\n\n\n\n\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

\n

Z3 in the Wild<\/h2>\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

Secret Sauce<\/h2>\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, Proof 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\n\n\n\n\n

There will be three days of informal talks and social activities including dinners scheduled for the evenings.<\/p>\n

PDF version of the program<\/a>.<\/p>\n

Wednesday, November 2<\/h3>\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n
9.00<\/td>\nWelcome & Breakfast<\/td>\n<\/tr>\n
9.30<\/td>\nTony Hoare<\/strong><\/td>\n<\/tr>\n
<\/td>\nThe Verified Software Initiative<\/td>\n<\/tr>\n
<\/td>\nHillel Kugler<\/strong><\/td>\n<\/tr>\n
<\/td>\nZ3 for Biology<\/td>\n<\/tr>\n
10.30<\/td>\nBreak<\/td>\n<\/tr>\n
11.00<\/td>\nThe Z3 Team<\/strong><\/td>\n<\/tr>\n
<\/td>\nNew and future features of Z3 Slides 1<\/a> Slides 2<\/a><\/td>\n<\/tr>\n
12.00<\/td>\nLunch<\/td>\n<\/tr>\n
13.30<\/td>\nAdrien Champion<\/strong><\/td>\n<\/tr>\n
<\/td>\nAssumptio and Stuff: using Z3 in a collaborative parallel formal verification framework. Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nMarko K\u00e4\u00e4ramees<\/strong><\/td>\n<\/tr>\n
<\/td>\nSymbolic analysis of EFSM models for test generation using Z3 Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nJuhan Ernits<\/strong><\/td>\n<\/tr>\n
<\/td>\nApplication of Z3 in Consistency Based Diagnosis of Hybrid Systems and Beyond<\/td>\n<\/tr>\n
15.00<\/td>\nBreak<\/td>\n<\/tr>\n
15.30<\/td>\nMalte Schwerhoff<\/strong><\/td>\n<\/tr>\n
<\/td>\nComparing Verification Condition Generation with Symbolic Execution Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nJoseph N. Ruskiewicz<\/strong><\/td>\n<\/tr>\n
<\/td>\nUsing Debuggers to Understand Failed Verification Attempts<\/td>\n<\/tr>\n
<\/td>\nArlen Cox<\/strong><\/td>\n<\/tr>\n
<\/td>\nCounterexample Generation for Separation Logic Slides<\/a><\/td>\n<\/tr>\n
17.00<\/td>\nClose<\/td>\n<\/tr>\n
18.00<\/td>\nCoach to pick up attendees from MSRC<\/td>\n<\/tr>\n
19.00<\/td>\nEvening Dinner at Restaurant Alimentum<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

 <\/p>\n

Thursday, November 3<\/h3>\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n
9.00<\/td>\nWelcome & Breakfast<\/td>\n<\/tr>\n
9.30<\/td>\nByron Cook<\/strong><\/td>\n<\/tr>\n
<\/td>\nSymbolic software model checking with Z3<\/td>\n<\/tr>\n
<\/td>\nAndrey Rybalchenko<\/strong><\/td>\n<\/tr>\n
<\/td>\nTowards Automatic Synthesis of Software Verification Tools<\/td>\n<\/tr>\n
10.30<\/td>\nBreak<\/td>\n<\/tr>\n
11.00<\/td>\nNik Sultana<\/strong><\/td>\n<\/tr>\n
<\/td>\nSolving trust issues using Z3 Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nAlexander Malkis<\/strong><\/td>\n<\/tr>\n
<\/td>\nAutomatic verification of software barriers: Z3 vs. MONA vs. BAPA.<\/td>\n<\/tr>\n
12.00<\/td>\nLunch<\/td>\n<\/tr>\n
13.30<\/td>\nChantal Keller<\/strong><\/td>\n<\/tr>\n
<\/td>\nCertification of SMT proof witnesses in the Coq proof assistant Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nTjark Weber<\/strong><\/td>\n<\/tr>\n
<\/td>\nIndependent Proof Reconstruction for Z3: An Overview<\/td>\n<\/tr>\n
<\/td>\nSascha Boehme<\/strong><\/td>\n<\/tr>\n
<\/td>\nProof Automation for Isabelle via Z3<\/td>\n<\/tr>\n
15.00<\/td>\nBreak<\/td>\n<\/tr>\n
15.30<\/td>\nJasmin Blanchette<\/strong><\/td>\n<\/tr>\n
<\/td>\nSledgehammer with Z3 Makes Isabelle Happy<\/td>\n<\/tr>\n
<\/td>\nKonstantin Korovin and Christoph Sticksel<\/strong><\/td>\n<\/tr>\n
<\/td>\nZ3 for iProver-Eq: efficient ground solving for instantiation-based first-order reasoning Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nPhilippe Suter<\/strong><\/td>\n<\/tr>\n
<\/td>\nProgramming with Z3<\/td>\n<\/tr>\n
17.00<\/td>\nClose<\/td>\n<\/tr>\n
19.00<\/td>\nEvening Dinner at Corpus Christi College<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

Friday, November 4<\/h3>\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n\n
9.00<\/td>\nWelcome & Breakfast<\/td>\n<\/tr>\n
9.30<\/td>\nCarsten Fuhs<\/strong><\/td>\n<\/tr>\n
<\/td>\nAutomated Termination Analysis for Programming Languages via Non-Linear SMT and Term Rewriting<\/td>\n<\/tr>\n
<\/td>\nSilvio Ranise<\/strong><\/td>\n<\/tr>\n
<\/td>\nSymbolic Backward Reachability with Effectively Propositional Logic<\/td>\n<\/tr>\n
10.30<\/td>\nBreak<\/td>\n<\/tr>\n
11.00<\/td>\nPaul Jackson<\/strong><\/td>\n<\/tr>\n
<\/td>\nProving SPARK-Ada verification conditions using SMT solvers<\/td>\n<\/tr>\n
<\/td>\nMargus Veanes<\/strong><\/td>\n<\/tr>\n
<\/td>\nMicrosoft.Automata library: application to Bek<\/td>\n<\/tr>\n
12.00<\/td>\nLunch<\/td>\n<\/tr>\n
13.30<\/td>\nSwen Jacobs<\/strong><\/td>\n<\/tr>\n
<\/td>\nSMT-based Reactive Synthesis<\/td>\n<\/tr>\n
<\/td>\nMarek Trtik<\/strong><\/td>\n<\/tr>\n
<\/td>\nOverapproximating Program Paths using FOL Formula Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nMaria Paola Bonacina<\/strong><\/td>\n<\/tr>\n
<\/td>\nTowards an interpolating DPLL(Gamma+T) Slides<\/a><\/td>\n<\/tr>\n
15.00<\/td>\nBreak<\/td>\n<\/tr>\n
15.30<\/td>\nVladimir Klebanov<\/strong><\/td>\n<\/tr>\n
<\/td>\nTheory reasoning in deductive program verification Slides<\/a><\/td>\n<\/tr>\n
<\/td>\nDenis Nicole<\/strong><\/td>\n<\/tr>\n
<\/td>\nThe ESBMC model checker for multi-threaded C<\/td>\n<\/tr>\n
17.00<\/td>\nClose<\/td>\n<\/tr>\n
19.00<\/td>\nPub crawl<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n\n\n","tab-content":[{"id":0,"name":"About","content":"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.\r\n
\r\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, Proof 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>"},{"id":1,"name":"Program","content":"There will be three days of informal talks and social activities including dinners scheduled for the evenings.\r\n\r\nPDF version of the program<\/a>.\r\n

Wednesday,\u00a0November 2<\/h3>\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n
9.00<\/td>\r\nWelcome & Breakfast<\/td>\r\n<\/tr>\r\n
9.30<\/td>\r\nTony Hoare<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nThe Verified Software Initiative<\/td>\r\n<\/tr>\r\n
<\/td>\r\nHillel Kugler<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nZ3 for Biology<\/td>\r\n<\/tr>\r\n
10.30<\/td>\r\nBreak<\/td>\r\n<\/tr>\r\n
11.00<\/td>\r\nThe Z3 Team<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nNew and future features of Z3 Slides 1<\/a>\u00a0Slides 2<\/a><\/td>\r\n<\/tr>\r\n
12.00<\/td>\r\nLunch<\/td>\r\n<\/tr>\r\n
13.30<\/td>\r\nAdrien Champion<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nAssumptio and Stuff: using Z3 in a collaborative parallel formal verification framework. Slides<\/a><\/td>\r\n<\/tr>\r\n
<\/td>\r\nMarko K\u00e4\u00e4ramees<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nSymbolic analysis of EFSM models for test generation using Z3 Slides<\/a><\/td>\r\n<\/tr>\r\n
<\/td>\r\nJuhan Ernits<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nApplication of Z3 in Consistency Based Diagnosis of Hybrid Systems and Beyond<\/td>\r\n<\/tr>\r\n
15.00<\/td>\r\nBreak<\/td>\r\n<\/tr>\r\n
15.30<\/td>\r\nMalte Schwerhoff<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nComparing Verification Condition Generation with Symbolic Execution Slides<\/a><\/td>\r\n<\/tr>\r\n
<\/td>\r\nJoseph N. Ruskiewicz<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nUsing Debuggers to Understand Failed Verification Attempts<\/td>\r\n<\/tr>\r\n
<\/td>\r\nArlen Cox<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nCounterexample Generation for Separation Logic Slides<\/a><\/td>\r\n<\/tr>\r\n
17.00<\/td>\r\nClose<\/td>\r\n<\/tr>\r\n
18.00<\/td>\r\nCoach to pick up attendees from MSRC<\/td>\r\n<\/tr>\r\n
19.00<\/td>\r\nEvening Dinner at Restaurant Alimentum<\/td>\r\n<\/tr>\r\n<\/tbody>\r\n<\/table>\r\n \r\n

Thursday, November 3<\/h3>\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n
9.00<\/td>\r\nWelcome & Breakfast<\/td>\r\n<\/tr>\r\n
9.30<\/td>\r\nByron Cook<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nSymbolic software model checking with Z3<\/td>\r\n<\/tr>\r\n
<\/td>\r\nAndrey Rybalchenko<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nTowards Automatic Synthesis of Software Verification Tools<\/td>\r\n<\/tr>\r\n
10.30<\/td>\r\nBreak<\/td>\r\n<\/tr>\r\n
11.00<\/td>\r\nNik Sultana<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nSolving trust issues using Z3 Slides<\/a><\/td>\r\n<\/tr>\r\n
<\/td>\r\nAlexander Malkis<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nAutomatic verification of software barriers: Z3 vs. MONA vs. BAPA.<\/td>\r\n<\/tr>\r\n
12.00<\/td>\r\nLunch<\/td>\r\n<\/tr>\r\n
13.30<\/td>\r\nChantal Keller<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nCertification of SMT proof witnesses in the Coq proof assistant Slides<\/a><\/td>\r\n<\/tr>\r\n
<\/td>\r\nTjark Weber<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nIndependent Proof Reconstruction for Z3: An Overview<\/td>\r\n<\/tr>\r\n
<\/td>\r\nSascha Boehme<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nProof Automation for Isabelle via Z3<\/td>\r\n<\/tr>\r\n
15.00<\/td>\r\nBreak<\/td>\r\n<\/tr>\r\n
15.30<\/td>\r\nJasmin Blanchette<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nSledgehammer with Z3 Makes Isabelle Happy<\/td>\r\n<\/tr>\r\n
<\/td>\r\nKonstantin Korovin and Christoph Sticksel<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nZ3 for iProver-Eq: efficient ground solving for instantiation-based first-order reasoning Slides<\/a><\/td>\r\n<\/tr>\r\n
<\/td>\r\nPhilippe Suter<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nProgramming with Z3<\/td>\r\n<\/tr>\r\n
17.00<\/td>\r\nClose<\/td>\r\n<\/tr>\r\n
19.00<\/td>\r\nEvening Dinner at Corpus Christi College<\/td>\r\n<\/tr>\r\n<\/tbody>\r\n<\/table>\r\n

Friday, November 4<\/h3>\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n\r\n
9.00<\/td>\r\nWelcome & Breakfast<\/td>\r\n<\/tr>\r\n
9.30<\/td>\r\nCarsten Fuhs<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nAutomated Termination Analysis for Programming Languages via Non-Linear SMT and Term Rewriting<\/td>\r\n<\/tr>\r\n
<\/td>\r\nSilvio Ranise<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nSymbolic Backward Reachability with Effectively Propositional Logic<\/td>\r\n<\/tr>\r\n
10.30<\/td>\r\nBreak<\/td>\r\n<\/tr>\r\n
11.00<\/td>\r\nPaul Jackson<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nProving SPARK-Ada verification conditions using SMT solvers<\/td>\r\n<\/tr>\r\n
<\/td>\r\nMargus Veanes<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nMicrosoft.Automata library: application to Bek<\/td>\r\n<\/tr>\r\n
12.00<\/td>\r\nLunch<\/td>\r\n<\/tr>\r\n
13.30<\/td>\r\nSwen Jacobs<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nSMT-based Reactive Synthesis<\/td>\r\n<\/tr>\r\n
<\/td>\r\nMarek Trtik<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nOverapproximating Program Paths using FOL Formula Slides<\/a><\/td>\r\n<\/tr>\r\n
<\/td>\r\nMaria Paola Bonacina<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nTowards an interpolating DPLL(Gamma+T) Slides<\/a><\/td>\r\n<\/tr>\r\n
15.00<\/td>\r\nBreak<\/td>\r\n<\/tr>\r\n
15.30<\/td>\r\nVladimir Klebanov<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nTheory reasoning in deductive program verification Slides<\/a><\/td>\r\n<\/tr>\r\n
<\/td>\r\nDenis Nicole<\/strong><\/td>\r\n<\/tr>\r\n
<\/td>\r\nThe ESBMC model checker for multi-threaded C<\/td>\r\n<\/tr>\r\n
17.00<\/td>\r\nClose<\/td>\r\n<\/tr>\r\n
19.00<\/td>\r\nPub crawl<\/td>\r\n<\/tr>\r\n<\/tbody>\r\n<\/table>"}],"msr_startdate":"2011-11-02","msr_enddate":"2011-11-04","msr_event_time":"","msr_location":"Microsoft Research, Cambridge","msr_event_link":"","msr_event_recording_link":"","msr_startdate_formatted":"November 2, 2011","msr_register_text":"Watch now","msr_cta_link":"","msr_cta_text":"","msr_cta_bi_name":"","featured_image_thumbnail":null,"event_excerpt":"This meeting is an opportunity for researchers to exchange experiences with others and the developers of Z3.","msr_research_lab":[],"related-researchers":[{"type":"user_nicename","display_name":"Nikolaj Bj\u00f8rner","user_id":33067,"people_section":"Group 1","alias":"nbjorner"}],"msr_impact_theme":[],"related-academic-programs":[],"related-groups":[],"related-projects":[],"related-opportunities":[],"related-publications":[],"related-videos":[],"related-posts":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/251948","targetHints":{"allow":["GET"]}}],"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":3,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/251948\/revisions"}],"predecessor-version":[{"id":874410,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/251948\/revisions\/874410"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=251948"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=251948"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=251948"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=251948"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=251948"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=251948"},{"taxonomy":"msr-program-audience","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-program-audience?post=251948"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=251948"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=251948"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}