{"id":199642,"date":"2008-12-12T12:46:39","date_gmt":"2008-12-12T12:46:39","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/events\/summer-school-on-programming-languages-analysis-and-verification\/"},"modified":"2025-08-06T12:03:04","modified_gmt":"2025-08-06T19:03:04","slug":"summer-school-on-programming-languages-analysis-and-verification","status":"publish","type":"msr-event","link":"https:\/\/www.microsoft.com\/en-us\/research\/event\/summer-school-on-programming-languages-analysis-and-verification\/","title":{"rendered":"Summer School on Programming Languages, Analysis, and Verification"},"content":{"rendered":"\n\n<p>Microsoft Research India, in collaboration with the Indian Institute of Science, conducted the Microsoft Research India Summer School on Programming Languages, Analysis and Verification from\u00a0June 16 to June 28, 2008, at the Indian Institute of Science, Bangalore.<\/p>\n<h3>India Schools<\/h3>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/lab\/microsoft-research-india\/\">Microsoft Research India<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/event\/2011-summer-school-security-privacy\/\" target=\"_self\">India Summer School on Security and Privacy 2011<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/event\/2011-school-approximability\/\">India School on Approximability 2011<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/event\/summer-school-computing-socio-economic-development\/\" target=\"_self\">India Summer School on Computing for Socio-Economic Development 2010<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/event\/summer-school-on-networking\/\">India Summer School on Networking 2009<\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<h2>About Summer School<\/h2>\n<p>The summer school consists of lectures by leading experts in the field from around the world. The aim of the school is to introduce students and young researchers to important new areas and the latest results in programming languages, program analysis, and software verification. The school aims to bring the state of the art in research in this area to senior undergraduate students, graduate students, research scholars and faculty members, and to provide a forum for Indian and international researchers to interact.<\/p>\n<p>The participants are expected to have reasonable exposure to the fundamental ideas in programming languages to derive maximum benefit from the lectures. Undergraduate courses in compilers, automata theory and logic are recommended as prerequisites. However, if you have exposure in only some of these prerequisites, and have sufficient enthusiasm about this research area to learn, you can benefit from the school. The lectures are designed to offer self-contained introductions to chosen topics, leading up to some open problems for research.<\/p>\n<p>We wish to emphasize here that this is not a lecture series covering the syllabus of any university course&#8211;the objective of the summer school is to bring to the participants the latest research results in the area, and help get them started in doing research.<\/p>\n<p>We hope to scribe these lectures, edit these notes and produce a volume that would be made available along with some Web materials. The participants may be expected to write surveys\/ tutorials\/ Web materials or interact with speakers on various research problems of mutual interest.\u00a0Microsoft Research\u00a0India will support travel and board for a few faculty members and for about 50 to 60 students.<\/p>\n<h2>Program Committee<\/h2>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" target=\"_blank\" href=\"http:\/\/www.cse.iitb.ac.in\/~supratik\/\">Supratik Chakraborty, IIT Bombay<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" target=\"_blank\" href=\"http:\/\/drona.csa.iisc.ernet.in\/~deepakd\/\">Deepak D\u2019Souza, IISc<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/sriram\/\">Sriram Rajamani,\u00a0Microsoft Research India<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/grama\/\">G Ramalingam, Microsoft Research India<\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<p><b>June 16 &#8211; <\/b><b>Preparatory lectures<\/b><\/p>\n<p><b>June 17\u201321<\/b><\/p>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/qadeer\/\"><b>Shaz Qadeer<\/b><\/a>, Taming Concurrency: A Program Verification Perspective, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/qadeer.pdf\"><b>slides<\/b><\/a> (pdf)<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" target=\"_blank\" href=\"http:\/\/www.cs.washington.edu\/homes\/djg\/\"><b>Dan Grossman<\/b><span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, Programming-Language Motivation, Design, and Semantics for Software Transactions, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/grossman.pdf\"><b>slides<\/b><\/a> (pdf)<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" target=\"_blank\" href=\"http:\/\/www.cs.umd.edu\/~jfoster\/\"><b>Jeff Foster<\/b><span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, Improving Software Quality with Type Qualifiers, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster1.pdf\"><b>slides-part1<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster2.pdf\"><b>slides-part2<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster3.pdf\"><b>slides-part3<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/miniqual2.tar.gz\"><b>miniqual code<\/b><\/a> (for programming exercise), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster-notes-wed.txt\"><b>notes from Wednesday<\/b><\/a> (txt)<\/li>\n<\/ul>\n<p><b>June 23 &#8211; <\/b><b>Preparatory lectures<\/b><\/p>\n<p><b>June 24-28<\/b><\/p>\n<ul>\n<li><b>Tim Harris<\/b>, Implementing Software Transactions, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/harris1.pdf\"><b>slides-intro<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/harris2.pdf\"><b>slides-main<\/b><\/a> (pdf)<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\"><b>Nikolaj Bjorner<\/b><\/a>, SMT solvers in Program Analysis and Verification<\/li>\n<li><b>Hongseok Yang<\/b>, Program Verification Using Separation Logic <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang0.pdf\"><b>lecture0-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang1.pdf\"><b>lecture1-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang2.pdf\"><b>lecture2-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang3.pdf\"><b>lecture3-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/peterslides.pdf\"><b>lecture4-slides (courtesy Peter O&#8217;Hearn)<\/b><\/a> (pdf)<\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Microsoft Research India, in collaboration with the Indian Institute of Science, conducted the Microsoft Research India Summer School on Programming Languages, Analysis and Verification from\u00a0June 16 to June 28, 2008, at the Indian Institute of Science, Bangalore. India Schools Microsoft Research India India Summer School on Security and Privacy 2011 India School on Approximability 2011 [&hellip;]<\/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":"2008-06-16","msr_enddate":"2008-06-28","msr_location":"Bangalore, India","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":[13560],"msr-region":[],"msr-event-type":[197941],"msr-video-type":[],"msr-locale":[268875],"msr-program-audience":[],"msr-post-option":[],"msr-impact-theme":[],"class_list":["post-199642","msr-event","type-msr-event","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-event-type-conferences","msr-locale-en_us"],"msr_about":"<!-- wp:msr\/event-details {\"title\":\"Summer School on Programming Languages, Analysis, and Verification\",\"backgroundColor\":\"grey\"} \/-->\n\n<!-- wp:msr\/content-tabs --><!-- wp:msr\/content-tab {\"title\":\"About\"} --><!-- wp:freeform --><p>Microsoft Research India, in collaboration with the Indian Institute of Science, conducted the Microsoft Research India Summer School on Programming Languages, Analysis and Verification from\u00a0June 16 to June 28, 2008, at the Indian Institute of Science, Bangalore.<\/p>\n<h3>India Schools<\/h3>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/lab\/microsoft-research-india\/\">Microsoft Research India<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/event\/2011-summer-school-security-privacy\/\" target=\"_self\">India Summer School on Security and Privacy 2011<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/event\/2011-school-approximability\/\">India School on Approximability 2011<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/event\/summer-school-computing-socio-economic-development\/\" target=\"_self\">India Summer School on Computing for Socio-Economic Development 2010<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/event\/summer-school-on-networking\/\">India Summer School on Networking 2009<\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<h2>About Summer School<\/h2>\n<p>The summer school consists of lectures by leading experts in the field from around the world. The aim of the school is to introduce students and young researchers to important new areas and the latest results in programming languages, program analysis, and software verification. The school aims to bring the state of the art in research in this area to senior undergraduate students, graduate students, research scholars and faculty members, and to provide a forum for Indian and international researchers to interact.<\/p>\n<p>The participants are expected to have reasonable exposure to the fundamental ideas in programming languages to derive maximum benefit from the lectures. Undergraduate courses in compilers, automata theory and logic are recommended as prerequisites. However, if you have exposure in only some of these prerequisites, and have sufficient enthusiasm about this research area to learn, you can benefit from the school. The lectures are designed to offer self-contained introductions to chosen topics, leading up to some open problems for research.<\/p>\n<p>We wish to emphasize here that this is not a lecture series covering the syllabus of any university course&#8211;the objective of the summer school is to bring to the participants the latest research results in the area, and help get them started in doing research.<\/p>\n<p>We hope to scribe these lectures, edit these notes and produce a volume that would be made available along with some Web materials. The participants may be expected to write surveys\/ tutorials\/ Web materials or interact with speakers on various research problems of mutual interest.\u00a0Microsoft Research\u00a0India will support travel and board for a few faculty members and for about 50 to 60 students.<\/p>\n<h2>Program Committee<\/h2>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" target=\"_blank\" href=\"http:\/\/www.cse.iitb.ac.in\/~supratik\/\">Supratik Chakraborty, IIT Bombay<\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" target=\"_blank\" href=\"http:\/\/drona.csa.iisc.ernet.in\/~deepakd\/\">Deepak D\u2019Souza, IISc<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/sriram\/\">Sriram Rajamani,\u00a0Microsoft Research India<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/grama\/\">G Ramalingam, Microsoft Research India<\/a><\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<!-- \/wp:freeform --><!-- \/wp:msr\/content-tab --><!-- wp:msr\/content-tab {\"title\":\"Agenda with Abstracts\"} --><!-- wp:freeform --><p><b>June 16 &#8211; <\/b><b>Preparatory lectures<\/b><\/p>\n<p><b>June 17\u201321<\/b><\/p>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/qadeer\/\"><b>Shaz Qadeer<\/b><\/a>, Taming Concurrency: A Program Verification Perspective, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/qadeer.pdf\"><b>slides<\/b><\/a> (pdf)<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" target=\"_blank\" href=\"http:\/\/www.cs.washington.edu\/homes\/djg\/\"><b>Dan Grossman<\/b><\/a>, Programming-Language Motivation, Design, and Semantics for Software Transactions, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/grossman.pdf\"><b>slides<\/b><\/a> (pdf)<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" target=\"_blank\" href=\"http:\/\/www.cs.umd.edu\/~jfoster\/\"><b>Jeff Foster<\/b><\/a>, Improving Software Quality with Type Qualifiers, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster1.pdf\"><b>slides-part1<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster2.pdf\"><b>slides-part2<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster3.pdf\"><b>slides-part3<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/miniqual2.tar.gz\"><b>miniqual code<\/b><\/a> (for programming exercise), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster-notes-wed.txt\"><b>notes from Wednesday<\/b><\/a> (txt)<\/li>\n<\/ul>\n<p><b>June 23 &#8211; <\/b><b>Preparatory lectures<\/b><\/p>\n<p><b>June 24-28<\/b><\/p>\n<ul>\n<li><b>Tim Harris<\/b>, Implementing Software Transactions, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/harris1.pdf\"><b>slides-intro<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/harris2.pdf\"><b>slides-main<\/b><\/a> (pdf)<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\"><b>Nikolaj Bjorner<\/b><\/a>, SMT solvers in Program Analysis and Verification<\/li>\n<li><b>Hongseok Yang<\/b>, Program Verification Using Separation Logic <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang0.pdf\"><b>lecture0-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang1.pdf\"><b>lecture1-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang2.pdf\"><b>lecture2-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang3.pdf\"><b>lecture3-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/peterslides.pdf\"><b>lecture4-slides (courtesy Peter O&#8217;Hearn)<\/b><\/a> (pdf)<\/li>\n<\/ul>\n<p><span id=\"label-external-link\" class=\"sr-only\" aria-hidden=\"true\">Opens in a new tab<\/span><\/p>\n<!-- \/wp:freeform --><!-- \/wp:msr\/content-tab --><!-- \/wp:msr\/content-tabs -->","tab-content":[{"id":0,"name":"About","content":"<h2>About Summer School<\/h2>\r\nThe summer school consists of lectures by leading experts in the field from around the world. The aim of the school is to introduce students and young researchers to important new areas and the latest results in programming languages, program analysis, and software verification. The school aims to bring the state of the art in research in this area to senior undergraduate students, graduate students, research scholars and faculty members, and to provide a forum for Indian and international researchers to interact.\r\n\r\nThe participants are expected to have reasonable exposure to the fundamental ideas in programming languages to derive maximum benefit from the lectures. Undergraduate courses in compilers, automata theory and logic are recommended as prerequisites. However, if you have exposure in only some of these prerequisites, and have sufficient enthusiasm about this research area to learn, you can benefit from the school. The lectures are designed to offer self-contained introductions to chosen topics, leading up to some open problems for research.\r\n\r\nWe wish to emphasize here that this is not a lecture series covering the syllabus of any university course--the objective of the summer school is to bring to the participants the latest research results in the area, and help get them started in doing research.\r\n\r\nWe hope to scribe these lectures, edit these notes and produce a volume that would be made available along with some Web materials. The participants may be expected to write surveys\/ tutorials\/ Web materials or interact with speakers on various research problems of mutual interest.\u00a0Microsoft Research\u00a0India will support travel and board for a few faculty members and for about 50 to 60 students.\r\n<h2>Program Committee<\/h2>\r\n<ul>\r\n \t<li><a href=\"http:\/\/www.cse.iitb.ac.in\/~supratik\/\">Supratik Chakraborty, IIT Bombay<\/a><\/li>\r\n \t<li><a href=\"http:\/\/drona.csa.iisc.ernet.in\/~deepakd\/\">Deepak D\u2019Souza, IISc<\/a><\/li>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/sriram\/\">Sriram Rajamani,\u00a0Microsoft Research India<\/a><\/li>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/grama\/\">G Ramalingam, Microsoft Research India<\/a><\/li>\r\n<\/ul>"},{"id":1,"name":"Agenda with Abstracts","content":"<b>June 16 - <\/b><b>Preparatory lectures<\/b>\r\n\r\n<b>June 17\u201321<\/b>\r\n<ul>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/qadeer\/\"><b>Shaz Qadeer<\/b><\/a>, Taming Concurrency: A Program Verification Perspective, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/qadeer.pdf\"><b>slides<\/b><\/a> (pdf)<\/li>\r\n \t<li><a href=\"http:\/\/www.cs.washington.edu\/homes\/djg\/\"><b>Dan Grossman<\/b><\/a>, Programming-Language Motivation, Design, and Semantics for Software Transactions, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/grossman.pdf\"><b>slides<\/b><\/a> (pdf)<\/li>\r\n \t<li><a href=\"http:\/\/www.cs.umd.edu\/~jfoster\/\"><b>Jeff Foster<\/b><\/a>, Improving Software Quality with Type Qualifiers, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster1.pdf\"><b>slides-part1<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster2.pdf\"><b>slides-part2<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster3.pdf\"><b>slides-part3<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/miniqual2.tar.gz\"><b>miniqual code<\/b><\/a> (for programming exercise), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/foster-notes-wed.txt\"><b>notes from Wednesday<\/b><\/a> (txt)<\/li>\r\n<\/ul>\r\n<b>June 23 - <\/b><b>Preparatory lectures<\/b>\r\n\r\n<b>June 24-28<\/b>\r\n<ul>\r\n \t<li><b>Tim Harris<\/b>, Implementing Software Transactions, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/harris1.pdf\"><b>slides-intro<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/harris2.pdf\"><b>slides-main<\/b><\/a> (pdf)<\/li>\r\n \t<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/nbjorner\/\"><b>Nikolaj Bjorner<\/b><\/a>, SMT solvers in Program Analysis and Verification<\/li>\r\n \t<li><b>Hongseok Yang<\/b>, Program Verification Using Separation Logic <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang0.pdf\"><b>lecture0-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang1.pdf\"><b>lecture1-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang2.pdf\"><b>lecture2-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/yang3.pdf\"><b>lecture3-slides<\/b><\/a> (pdf), <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2008\/12\/peterslides.pdf\"><b>lecture4-slides (courtesy Peter O'Hearn)<\/b><\/a> (pdf)<\/li>\r\n<\/ul>"}],"msr_startdate":"2008-06-16","msr_enddate":"2008-06-28","msr_event_time":"","msr_location":"Bangalore, India","msr_event_link":"","msr_event_recording_link":"","msr_startdate_formatted":"June 16, 2008","msr_register_text":"Watch now","msr_cta_link":"","msr_cta_text":"","msr_cta_bi_name":"","featured_image_thumbnail":null,"event_excerpt":"About Summer School The summer school consists of lectures by leading experts in the field from around the world. The aim of the school is to introduce students and young researchers to important new areas and the latest results in programming languages, program analysis, and software verification. The school aims to bring the state of the art in research in this area to senior undergraduate students, graduate students, research scholars and faculty members, and to&hellip;","msr_research_lab":[199562],"related-researchers":[],"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\/199642","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":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/199642\/revisions"}],"predecessor-version":[{"id":1147455,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event\/199642\/revisions\/1147455"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=199642"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=199642"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=199642"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=199642"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=199642"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=199642"},{"taxonomy":"msr-program-audience","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-program-audience?post=199642"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=199642"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=199642"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}