{"id":1119,"date":"2021-05-17T09:14:26","date_gmt":"2021-05-17T01:14:26","guid":{"rendered":"http:\/\/lcs.ios.ac.cn\/fm2021\/?page_id=1119"},"modified":"2021-06-23T17:58:29","modified_gmt":"2021-06-23T09:58:29","slug":"i-day-invited-speakers","status":"publish","type":"page","link":"http:\/\/lcs.ios.ac.cn\/fm2021\/i-day-invited-speakers\/","title":{"rendered":"I-Day Invited Speakers"},"content":{"rendered":"<p><div class=\"fusion-fullwidth fullwidth-box fusion-builder-row-1 fusion-flex-container nonhundred-percent-fullwidth non-hundred-percent-height-scrolling\" style=\"background-color: rgba(255,255,255,0);background-position: center center;background-repeat: no-repeat;border-width: 0px 0px 0px 0px;border-color:#e2e2e2;border-style:solid;\" ><div class=\"fusion-builder-row fusion-row fusion-flex-align-items-flex-start\" style=\"max-width:1248px;margin-left: calc(-4% \/ 2 );margin-right: calc(-4% \/ 2 );\"><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-0 fusion_builder_column_1_5 1_5 fusion-flex-column\"><div class=\"fusion-column-wrapper fusion-flex-justify-content-flex-start fusion-content-layout-column\" style=\"background-position:left top;background-repeat:no-repeat;-webkit-background-size:cover;-moz-background-size:cover;-o-background-size:cover;background-size:cover;padding: 0px 0px 0px 0px;\"><div ><span class=\" fusion-imageframe imageframe-none imageframe-1 hover-type-none\"><img width=\"150\" height=\"150\" title=\"Carl-JohanSeger-750px\" src=\"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/05\/Carl-JohanSeger-750px-e1621213641702-150x150.jpg\" class=\"img-responsive wp-image-1116\"\/><\/span><\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-0{width:20% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-0 > .fusion-column-wrapper {padding-top : 0px !important;padding-right : 0px !important;margin-right : 9.6%;padding-bottom : 0px !important;padding-left : 0px !important;margin-left : 9.6%;}@media only screen and (max-width:1024px) {.fusion-body .fusion-builder-column-0{width:20% !important;order : 0;}.fusion-builder-column-0 > .fusion-column-wrapper {margin-right : 9.6%;margin-left : 9.6%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-0{width:100% !important;order : 0;}.fusion-builder-column-0 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-1 fusion_builder_column_4_5 4_5 fusion-flex-column\"><div class=\"fusion-column-wrapper fusion-flex-justify-content-flex-start fusion-content-layout-column\" style=\"background-position:left top;background-repeat:no-repeat;-webkit-background-size:cover;-moz-background-size:cover;-o-background-size:cover;background-size:cover;padding: 0px 0px 0px 0px;\"><div class=\"fusion-text fusion-text-1\"><div><strong>Name<\/strong>: Carl Seger<\/div>\n<div><strong>Title<\/strong>: Formal Verification of Complex Data-Paths: An Industrial Perspective<\/div>\n<div style=\"text-align: justify;\"><strong>Abstract<\/strong>: After caches, most transistors in a modern chip are devoted to wide data-paths. Due to performance and power requirements, these data-paths are often implementing sophisticated algorithms and use complex implementations. As Intel experienced in 1994, a bug in a data-path can be extremely expensive and thus needs to be avoided at almost any cost. At the same time, simulation based verification is extremely poor at verifying data-paths due to the vast data space and thus formal verification is appealing. In this talk we will give a retrospective on the formal verification of complex data-paths that took place at Intel from the mid-1990s until recently. We will discuss the technology that made the effort possible, the tools developed that made it feasible, and the methodology created that made it practical.<\/div>\n<div style=\"text-align: justify;\"><strong>Bio<\/strong>: Dr. Carl-Johan (Carl) Seger received his M.Sc. in Engineering Physics from Chalmers University of Technology, Sweden in 1985 and his M. Math and Ph.D. degrees in Computer Science from University of Waterloo, Canada, in 1986 and 1988 respectively.\u00a0 After seven years in academia, ending as associate professor at the University of British Columbia, Canada, he joined Intel Corporation's Strategic CAD Labs in 1995 where he stayed for more than 21 years.\u00a0 At Intel, Dr. Seger drove the development and successful wide deployment of formal verification of Intel's microprocessors.\u00a0 In 2006-2007 has was granted a full year sabbatical from Intel and became an Oliver Smithies lecturer and visiting fellow at Balliol College, Oxford.\u00a0 In 2016, he took early retirement from Intel and joined the Computer Science and Engineering department at Chalmers University of Technology as a WASP Professor. In addition to formal verification of hardware, Dr. Seger's research interests focuses on how to design and verify correct, robust, and secure software\/hardware systems for autonomous vehicles and other Internet-of-Things.<\/div>\n<\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-1{width:80% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-1 > .fusion-column-wrapper {padding-top : 0px !important;padding-right : 0px !important;margin-right : 2.4%;padding-bottom : 0px !important;padding-left : 0px !important;margin-left : 2.4%;}@media only screen and (max-width:1024px) {.fusion-body .fusion-builder-column-1{width:80% !important;order : 0;}.fusion-builder-column-1 > .fusion-column-wrapper {margin-right : 2.4%;margin-left : 2.4%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-1{width:100% !important;order : 0;}.fusion-builder-column-1 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-2 fusion_builder_column_1_1 1_1 fusion-flex-column\"><div class=\"fusion-column-wrapper fusion-flex-justify-content-flex-start fusion-content-layout-column\" style=\"background-position:left top;background-repeat:no-repeat;-webkit-background-size:cover;-moz-background-size:cover;-o-background-size:cover;background-size:cover;padding: 0px 0px 0px 0px;\"><div class=\"fusion-text fusion-text-2\"><hr \/>\n<\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-2{width:100% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-2 > .fusion-column-wrapper {padding-top : 0px !important;padding-right : 0px !important;margin-right : 1.92%;padding-bottom : 0px !important;padding-left : 0px !important;margin-left : 1.92%;}@media only screen and (max-width:1024px) {.fusion-body .fusion-builder-column-2{width:100% !important;order : 0;}.fusion-builder-column-2 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-2{width:100% !important;order : 0;}.fusion-builder-column-2 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><\/div><style type=\"text\/css\">.fusion-body .fusion-flex-container.fusion-builder-row-1{ padding-top : 0px;margin-top : 0px;padding-right : 0px;padding-bottom : 0px;margin-bottom : 0px;padding-left : 0px;}<\/style><\/div><div class=\"fusion-fullwidth fullwidth-box fusion-builder-row-2 fusion-flex-container nonhundred-percent-fullwidth non-hundred-percent-height-scrolling\" style=\"background-color: rgba(255,255,255,0);background-position: center center;background-repeat: no-repeat;border-width: 0px 0px 0px 0px;border-color:#e2e2e2;border-style:solid;\" ><div class=\"fusion-builder-row fusion-row fusion-flex-align-items-flex-start\" style=\"max-width:1248px;margin-left: calc(-4% \/ 2 );margin-right: calc(-4% \/ 2 );\"><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-3 fusion_builder_column_1_5 1_5 fusion-flex-column\"><div class=\"fusion-column-wrapper fusion-flex-justify-content-flex-start fusion-content-layout-column\" style=\"background-position:left top;background-repeat:no-repeat;-webkit-background-size:cover;-moz-background-size:cover;-o-background-size:cover;background-size:cover;padding: 0px 0px 0px 0px;\"><div ><span class=\" fusion-imageframe imageframe-none imageframe-2 hover-type-none\"><img width=\"150\" height=\"150\" title=\"grant-hi\" src=\"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/06\/grant-hi-150x150.png\" class=\"img-responsive wp-image-1132\"\/><\/span><\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-3{width:20% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-3 > .fusion-column-wrapper {padding-top : 0px !important;padding-right : 0px !important;margin-right : 9.6%;padding-bottom : 0px !important;padding-left : 0px !important;margin-left : 9.6%;}@media only screen and (max-width:1024px) {.fusion-body .fusion-builder-column-3{width:20% !important;order : 0;}.fusion-builder-column-3 > .fusion-column-wrapper {margin-right : 9.6%;margin-left : 9.6%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-3{width:100% !important;order : 0;}.fusion-builder-column-3 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-4 fusion_builder_column_4_5 4_5 fusion-flex-column\"><div class=\"fusion-column-wrapper fusion-flex-justify-content-flex-start fusion-content-layout-column\" style=\"background-position:left top;background-repeat:no-repeat;-webkit-background-size:cover;-moz-background-size:cover;-o-background-size:cover;background-size:cover;padding: 0px 0px 0px 0px;\"><div class=\"fusion-text fusion-text-3\"><div><strong>Name<\/strong>: Grant Passmore<\/div>\n<div><strong>Title<\/strong>: Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms<\/div>\n<div style=\"text-align: justify;\"><strong>Abstract<\/strong>: At Imandra Inc. we have pioneered the application of formal methods to financial algorithms. After nearly a decade of R&amp;D and business development, our Imandra automated reasoning system is now in mainstream use at major financial firms such as Goldman Sachs, Itiviti and OneChronos. In these settings, Imandra is relied upon for the design, verification, ongoing auditing and calibration of global financial infrastructure such as trading venues (exchanges and dark pools), smart order routers and FIX connectivity between trading systems. Getting to this point, however, was not an easy road. When we began, we faced a collection of simultaneous challenges. In this talk, we shall discuss these challenges and our solutions, with an eye towards open problems and the future.<\/div>\n<div style=\"text-align: justify;\"><strong>Bio<\/strong>: Grant Passmore is co-founder and co-CEO of Imandra. Grant is a widely published researcher in formal verification and symbolic AI, and has more than fifteen years\u2019 industrial formal verification experience. He has been a key contributor to safety verification of algorithms at Cambridge, Carnegie Mellon, Edinburgh, Microsoft Research and SRI. He earned his PhD from the University of Edinburgh, is a graduate of UT Austin (BA in Mathematics) and the Mathematical Research Institute in the Netherlands (Master Class in Mathematical Logic), and is a Life Member of Clare Hall, University of Cambridge.<\/div>\n<\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-4{width:80% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-4 > .fusion-column-wrapper {padding-top : 0px !important;padding-right : 0px !important;margin-right : 2.4%;padding-bottom : 0px !important;padding-left : 0px !important;margin-left : 2.4%;}@media only screen and (max-width:1024px) {.fusion-body .fusion-builder-column-4{width:80% !important;order : 0;}.fusion-builder-column-4 > .fusion-column-wrapper {margin-right : 2.4%;margin-left : 2.4%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-4{width:100% !important;order : 0;}.fusion-builder-column-4 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><\/div><style type=\"text\/css\">.fusion-body .fusion-flex-container.fusion-builder-row-2{ padding-top : 0px;margin-top : 0px;padding-right : 0px;padding-bottom : 0px;margin-bottom : 0px;padding-left : 0px;}<\/style><\/div><\/p>\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1119"}],"collection":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/comments?post=1119"}],"version-history":[{"count":10,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1119\/revisions"}],"predecessor-version":[{"id":1136,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1119\/revisions\/1136"}],"wp:attachment":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/media?parent=1119"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}