{"id":12,"date":"2020-06-03T07:46:53","date_gmt":"2020-06-03T07:46:53","guid":{"rendered":"http:\/\/easyconferences.eu\/itp2021\/?page_id=12"},"modified":"2021-06-09T13:00:02","modified_gmt":"2021-06-09T13:00:02","slug":"keynote-speakers","status":"publish","type":"page","link":"https:\/\/easyconferences.eu\/itp2021\/keynote-speakers\/","title":{"rendered":"Keynote Speakers"},"content":{"rendered":"<p>[et_pb_section fb_built=&#8221;1&#8243; next_background_color=&#8221;#ffffff&#8221; _builder_version=&#8221;4.4.6&#8243; background_color=&#8221;#8c8c8c&#8221; top_divider_color=&#8221;#b53319&#8243; bottom_divider_style=&#8221;arrow3&#8243;][et_pb_row _builder_version=&#8221;4.4.6&#8243; custom_margin=&#8221;-26px|auto||auto||&#8221;][et_pb_column type=&#8221;4_4&#8243; _builder_version=&#8221;4.4.6&#8243;][et_pb_text _builder_version=&#8221;4.4.6&#8243;]<\/p>\n<h2 style=\"text-align: center;\"><span style=\"color: #ffffff;\">Keynote Speakers<\/span><\/h2>\n<p>[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section][et_pb_section fb_built=&#8221;1&#8243; _builder_version=&#8221;4.4.6&#8243;][et_pb_row column_structure=&#8221;1_3,1_3,1_3&#8243; _builder_version=&#8221;4.4.6&#8243;][et_pb_column type=&#8221;1_3&#8243; _builder_version=&#8221;4.4.6&#8243;][et_pb_image src=&#8221;http:\/\/easyconferences.eu\/itp2021\/wp-content\/uploads\/2021\/03\/nadia.jpg&#8221; title_text=&#8221;Nadia Polikarpova&#8221; _builder_version=&#8221;4.4.6&#8243; width=&#8221;150%&#8221; max_width=&#8221;130%&#8221; height=&#8221;300px&#8221; max_height=&#8221;1000px&#8221; custom_padding=&#8221;|||65px||&#8221;][\/et_pb_image][et_pb_text _builder_version=&#8221;4.4.6&#8243;]<\/p>\n<h3 style=\"text-align: center;\"><span style=\"color: #003366;\">Nadia Polikarpova<\/span><\/h3>\n<p style=\"text-align: center;\">University of California, San Diego<\/p>\n<p style=\"text-align: center;\">(joint with LICS)<\/p>\n<p style=\"text-align: center;\">Title:\u00a0Synthesis of Safe Pointer-Manipulating Programs<\/p>\n<p style=\"text-align: center;\">Abstract:<\/p>\n<p>Low-level pointer-manipulating code is ubiquitous in operating systems, networking stacks, and browsers, which form the backbone of our digital infrastructure.<\/p>\n<p>Unfortunately, this code is susceptible to many kinds of bugs, which lead to crashes and security vulnerabilities.         <div class=\"rmwr-wrapper\" \n             data-id=\"rmwr-69e1b652ce522\"\n             data-mode=\"normal\"\n             data-animation=\"fade\"\n             data-duration=\"300\"\n             data-smooth-scroll=\"true\"\n             data-scroll-offset=\"0\">\n            <button \n                type=\"button\"\n                class=\"read-link\" \n                id=\"readlinkrmwr-69e1b652ce522\"\n                data-open-text=\"Read More\"\n                data-close-text=\"Read Less\"\n                aria-expanded=\"false\"\n                aria-controls=\"readrmwr-69e1b652ce522\"\n                aria-label=\"Read More\"\n            >\n                <span class=\"rmwr-text\">Read More<\/span>\n            <\/button>\n            <div \n                class=\"read_div\" \n                id=\"readrmwr-69e1b652ce522\"\n                aria-hidden=\"true\"\n                data-animation=\"fade\"\n                data-duration=\"300\"\n                style=\"display: none;\"\n            >\n                A promising approach to eliminating bugs and reducing programmer effort at the same time is to use program synthesis technology to generate provably correct low-level code automatically from high-level specifications.<\/p>\n<p>In this talk I will present a program synthesizer SuSLik, which accepts as input a specification written in separation logic, and produces as output a provably correct C program. SuSLik is the first synthesizer capable of generating a wide range of operations on linked data structures (such as singly- and doubly-linked lists, binary trees, and rose trees) without additional hints from the user. It is also the first synthesizer to automatically discover recursive auxiliary functions required for nested data structure traversal. To make this possible, SuSLik relies on a novel proof system-synthetic separation logic-to derive correct-by-construction programs directly from their specifications. Program proofs generated by SuSLik can be automatically translated into three foundational verification frameworks embedded in Coq: Hoare Type Theory (HTT), Iris, and Verified Software Toolchain (VST).            <\/div>\n        <\/div>\n        <\/p>\n<p>[\/et_pb_text][\/et_pb_column][et_pb_column type=&#8221;1_3&#8243; _builder_version=&#8221;4.4.6&#8243;][et_pb_image src=&#8221;http:\/\/easyconferences.eu\/itp2021\/wp-content\/uploads\/2021\/03\/Andrei_Popescu_2020.jpg&#8221; title_text=&#8221;Andrei_Popescu_2020&#8243; _builder_version=&#8221;4.4.6&#8243; custom_padding=&#8221;61px|||70px||&#8221; hover_enabled=&#8221;0&#8243; disabled_on=&#8221;off|off|off&#8221;][\/et_pb_image][et_pb_text _builder_version=&#8221;4.4.6&#8243; custom_margin=&#8221;93px|||||&#8221;]<\/p>\n<h3 style=\"text-align: center;\"><span style=\"color: #003366;\">Andrei Popescu<\/span><\/h3>\n<p style=\"text-align: center;\">University of Sheffield<\/p>\n<p style=\"text-align: center;\">Title:\u00a0Bounded-Deducibility Security<\/p>\n<p style=\"text-align: center;\">Abstract:<\/p>\n<p>Starting from 2013, together with colleagues I have developed a framework for the specification and verification of information-flow security. The framework is called Bounded-Deducibility (BD) Security because it generalises Sutherland&#8217;s notion of Nondeducibility: from entirely preventing to only bounding the allowed flows of information. It was born from the challenges of expressing fine-grained confidentiality policies, as required by many multi-user web-based systems.        <div class=\"rmwr-wrapper\" \n             data-id=\"rmwr-69e1b652ce639\"\n             data-mode=\"normal\"\n             data-animation=\"fade\"\n             data-duration=\"300\"\n             data-smooth-scroll=\"true\"\n             data-scroll-offset=\"0\">\n            <button \n                type=\"button\"\n                class=\"read-link\" \n                id=\"readlinkrmwr-69e1b652ce639\"\n                data-open-text=\"Read More\"\n                data-close-text=\"Read Less\"\n                aria-expanded=\"false\"\n                aria-controls=\"readrmwr-69e1b652ce639\"\n                aria-label=\"Read More\"\n            >\n                <span class=\"rmwr-text\">Read More<\/span>\n            <\/button>\n            <div \n                class=\"read_div\" \n                id=\"readrmwr-69e1b652ce639\"\n                aria-hidden=\"true\"\n                data-animation=\"fade\"\n                data-duration=\"300\"\n                style=\"display: none;\"\n            >\n                <\/p>\n<p>BD Security was formalised in the proof assistant Isabelle\/HOL and was used for verifying desirable confidentiality aspects of some running systems: CoCon, a practical conference management system that was deployed for two international conferences (one of them being the 2016 edition of ITP), CoSMed, a prototype social media platform, and CoSMeDis, a distributed extension of CoSMed (the last two developed in collaboration with a social media company). These systems were implemented from the ground up with verifiability in mind, using Isabelle\/HOL&#8217;s specification language and code generator.<\/p>\n<p>In this talk, I will describe the design principles behind BD Security and the eventful journey of deploying this framework to verify running systems. I will also discuss newer developments that further extend the framework&#8217;s flexibility and improve the resilience of verification code under system extensions with new features.<\/p>\n<p>Several colleagues have participated in various parts of this work:<br \/> Thomas Bauereiss, Sergey Grebenshchikov, Ping Hou, Peter Lammich, Sudeep Kanav, Ondrej Kuncar, Armando Pesenti Gritti and Franco Raimondi.            <\/div>\n        <\/div>\n        <\/p>\n<p>[\/et_pb_text][\/et_pb_column][et_pb_column type=&#8221;1_3&#8243; _builder_version=&#8221;4.4.6&#8243;][et_pb_image src=&#8221;http:\/\/easyconferences.eu\/itp2021\/wp-content\/uploads\/2021\/03\/me.jpg&#8221; title_text=&#8221;me&#8221; _builder_version=&#8221;4.4.6&#8243; height=&#8221;300px&#8221; custom_padding=&#8221;|||65px||&#8221;][\/et_pb_image][et_pb_text _builder_version=&#8221;4.4.6&#8243;]<\/p>\n<h3 style=\"text-align: center;\"><span style=\"color: #003366;\">Magnus Myreen<\/span><\/h3>\n<p style=\"text-align: center;\">Chalmers<\/p>\n<p style=\"text-align: center;\">Title:\u00a0The CakeML Project\u2019s Quest for Ever Stronger Correctness Theorems<\/p>\n<p style=\"text-align: center;\">Abstract:<\/p>\n<p>The CakeML project has developed a proof-producing code generation<br \/> mechanism for HOL4, a verified compiler for ML and, using these, a number of verified application programs that are proved correct down to the machine code that runs them.         <div class=\"rmwr-wrapper\" \n             data-id=\"rmwr-69e1b652ce68a\"\n             data-mode=\"normal\"\n             data-animation=\"fade\"\n             data-duration=\"300\"\n             data-smooth-scroll=\"true\"\n             data-scroll-offset=\"0\">\n            <button \n                type=\"button\"\n                class=\"read-link\" \n                id=\"readlinkrmwr-69e1b652ce68a\"\n                data-open-text=\"Read More\"\n                data-close-text=\"Read Less\"\n                aria-expanded=\"false\"\n                aria-controls=\"readrmwr-69e1b652ce68a\"\n                aria-label=\"Read More\"\n            >\n                <span class=\"rmwr-text\">Read More<\/span>\n            <\/button>\n            <div \n                class=\"read_div\" \n                id=\"readrmwr-69e1b652ce68a\"\n                aria-hidden=\"true\"\n                data-animation=\"fade\"\n                data-duration=\"300\"\n                style=\"display: none;\"\n            >\n                <\/p>\n<p>In this talk, I will tell the story behind the project, point curious listerners to papers where they can read more about specific parts; and I will share some thoughts on where the<br \/> project might go next.            <\/div>\n        <\/div>\n        <\/p>\n<p>[\/et_pb_text][\/et_pb_column][\/et_pb_row][\/et_pb_section]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Keynote SpeakersNadia Polikarpova University of California, San Diego (joint with LICS) Title:\u00a0Synthesis of Safe Pointer-Manipulating Programs Abstract: Low-level pointer-manipulating code is ubiquitous in operating systems, networking stacks, and browsers, which form the backbone of our digital infrastructure. Unfortunately, this code is susceptible to many kinds of bugs, which lead to crashes and security vulnerabilities. <\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_et_pb_use_builder":"on","_et_pb_old_content":"<!-- wp:divi\/placeholder \/-->","_et_gb_content_width":""},"_links":{"self":[{"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/pages\/12"}],"collection":[{"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/comments?post=12"}],"version-history":[{"count":32,"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/pages\/12\/revisions"}],"predecessor-version":[{"id":489,"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/pages\/12\/revisions\/489"}],"wp:attachment":[{"href":"https:\/\/easyconferences.eu\/itp2021\/wp-json\/wp\/v2\/media?parent=12"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}