{"id":1019,"date":"2021-03-08T13:44:07","date_gmt":"2021-03-08T05:44:07","guid":{"rendered":"http:\/\/lcs.ios.ac.cn\/fm2021\/?page_id=1019"},"modified":"2021-11-02T13:18:35","modified_gmt":"2021-11-02T05:18:35","slug":"invited-speakers","status":"publish","type":"page","link":"http:\/\/lcs.ios.ac.cn\/fm2021\/invited-speakers\/","title":{"rendered":"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=\"mingshengying\" src=\"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/mingshengying-150x150.jpg\" class=\"img-responsive wp-image-1022\"\/><\/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>: Mingsheng Ying<\/div>\n<div><strong>Title<\/strong>: <em>Model Checking for Verification of Quantum Circuits<\/em><\/div>\n<div style=\"text-align: justify;\"><strong>Abstract<\/strong>: In this talk, I will describe a framework for assertion-based verification of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which:<\/div>\n<div style=\"text-align: justify;\">(1) noiseless and noisy quantum circuits are modelled as quantum automata and quantum Markov chains, respectively, and they are further represented by tensor networks;<\/div>\n<div style=\"text-align: justify;\">(2) Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic;<\/div>\n<div style=\"text-align: justify;\">(3) Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks.<\/div>\n<div style=\"text-align: justify;\"><strong>Bio<\/strong>: Mingsheng Ying is a Distinguished Professor and Research Director of the Center for Quantum Software<span lang=\"en-US\">\u00a0<\/span><span lang=\"en-US\">\u00a0<\/span><span lang=\"en-US\">and Information at the University of Technology Sydney, Australia. He is also Deputy Director for Research (adjunct position) at the Institute of Software at the Chinese Academy of Sciences, and holds the Cheung Kong Chair Professorship at Tsinghua University, China. Ying was also the Director of the Scientific Committee of the National Key Laboratory of Intelligent Technology and Systems at Tsinghua University. His research interests include quantum computation, theory of programming languages, and<\/span><span lang=\"en-US\">\u00a0<\/span><span lang=\"en-US\">logics in<\/span><span lang=\"en-US\">\u00a0<\/span><span lang=\"en-US\">AI. He has published books:<\/span><span lang=\"en-US\">\u00a0Model Checking Quantum Systems: Principles and Algorithms (2021) (with Yuan Feng),\u00a0<\/span><span lang=\"en-US\"><i>Foundations of Quantum Programming\u00a0<\/i><\/span><span lang=\"en-US\">(2016) and<\/span><span lang=\"en-US\">\u00a0<\/span><span lang=\"en-US\"><i>Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs<\/i><\/span><span lang=\"en-US\"><i>\u00a0<\/i><\/span><span lang=\"en-US\">(2001).<\/span><\/div>\n<div><span style=\"font-family: Calibri,sans-serif; font-size: small; text-align: justify;\"><span lang=\"en-US\">Ying received a China National Science Award in Natural Science (2008). He has served on the editorial board of several publications including<\/span><span lang=\"en-US\">\u00a0<\/span><span lang=\"en-US\"><i>Artificial Intelligence Journal<\/i><\/span><span lang=\"en-US\">. He is currently Editor-in-Chief of<\/span><span lang=\"en-US\">\u00a0<\/span><span lang=\"en-US\"><i>ACM<\/i><\/span><span lang=\"en-US\"><i>\u00a0<\/i><\/span><a href=\"https:\/\/tqc.acm.org\/\" target=\"_blank\" rel=\"noopener\"><span style=\"color: #954f72;\"><span lang=\"en-US\"><i>Transactions on Quantum Computing<\/i><\/span><\/span><\/a><span lang=\"en-US\">.<\/span><span lang=\"en-US\">\u00a0<\/span><\/span><\/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><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-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-2{ 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-3 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=\"paula-herber-200x250\" src=\"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/paula-herber-200x250-1-150x150.jpg\" class=\"img-responsive wp-image-1037\"\/><\/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:\u00a0\u00a0<\/strong>Paula Herber<\/div>\n<div><b>Title:\u00a0<\/b><em>Combine Forces - How to Formally Verify Informally Defined Embedded Systems<\/em><\/div>\n<div style=\"text-align: justify;\"><b>Abstract:<\/b>\u00a0Embedded systems are ubiquitous in our everyday lives, and they are often used in safety-critical applications, such as cars, airplanes, or medical systems. As a consequence, there is a high demand for formal methods to ensure their safety. Embedded systems are, however, concurrent, real-time dependent, and highly heterogeneous. Hardware and software are deeply intertwined, and the digital control parts interact with an analogous environment. Moreover, the semantics of industrially used embedded system design languages, such as Matlab\/Simulink or SystemC, is typically only informally defined. To formally capture informally defined embedded systems requires a deep understanding of the underlying models of computation. Furthermore, a single formalism and verification tool are typically not powerful enough to cope with the heterogeneity of embedded systems. In this talk, I summarize our work on automated transformations from informal system descriptions into existing formal verification tools. I present ideas to combine the strengths of various languages, formalisms, and verification backends, and discuss promising results, challenges and limitations.<\/div>\n<div style=\"text-align: justify;\"><b>Short Bio: <\/b>Prof. Dr.-Ing. Paula Herber received her Ph.D. from TU Berlin in 2010. She worked as a postdoc at the International Computer Science Institute (ICSI) in Berkeley, California, as a substitute professor at the University of Potsdam, and as a postdoc and independent research group leader in the Software Engineering and Embedded Systems group at TU Berlin. Since October 2018, she is a full professor at the University of M\u00fcnster and head of the Embedded Systems Group at the Computer Science Department. Her main research interests are quality assurance for embedded systems, test automation, and formal methods.<\/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-3{ 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-4 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-5 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-4\"><hr \/>\n<\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-5{width:100% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-5 > .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-5{width:100% !important;order : 0;}.fusion-builder-column-5 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-5{width:100% !important;order : 0;}.fusion-builder-column-5 > .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-4{ 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-5 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-6 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-3 hover-type-none\"><img width=\"150\" height=\"150\" title=\"clark\" src=\"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/clark-150x150.jpg\" class=\"img-responsive wp-image-1026\" srcset=\"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/clark-200x200.jpg 200w, http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/clark-400x400.jpg 400w, http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/clark-600x600.jpg 600w, http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/clark-800x800.jpg 800w, http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/clark-1200x1200.jpg 1200w, http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/clark.jpg 1920w\" sizes=\"(max-width: 640px) 100vw, 200px\" \/><\/span><\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-6{width:20% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-6 > .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-6{width:20% !important;order : 0;}.fusion-builder-column-6 > .fusion-column-wrapper {margin-right : 9.6%;margin-left : 9.6%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-6{width:100% !important;order : 0;}.fusion-builder-column-6 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-7 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-5\"><div id=\"Clark\"><strong>Name<\/strong>: Clark Barrett<\/div>\n<div><strong>Title<\/strong>: <em>Domain-Specific Reasoning with Satisfiability Modulo Theories<\/em><\/div>\n<div style=\"text-align: justify;\"><strong>Abstract<\/strong>: General-purpose automated reasoning approaches such as automated theorem proving (ATP) and Boolean satisfiability (SAT) are extremely versatile. Many interesting and practical problems can be reduced to ATP or SAT problems. On the other hand, these techniques cannot easily incorporate customized domain-specific reasoning. In contrast, this is one of the strengths of approaches based on satisfiabiilty modulo theories (SMT). This talk showcases recent work in which domain-specific customization of SMT solvers plays a key role in making otherwise intractable problems tractable. The domains discussed include reasoning about neural networks and reasoning about string constraints.<\/div>\n<div style=\"text-align: justify;\"><strong>Short Bio<\/strong>: Clark Barrett joined Stanford University as an Associate Professor (Research) of Computer Science in September 2016. Before that, he was an Associate Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University. His expertise is in constraint solving and its applications to system verification and security. His PhD dissertation introduced a novel approach to constraint solving now known as Satisfiability Modulo Theories (SMT). Today, he is recognized as one of the world's experts in the development and application of SMT techniques. He was also an early pioneer in the development of formal hardware verification: at Intel, he collaborated on a novel theorem prover used to verify key microprocessor properties; and at 0-in Design Automation (now part of Mentor Graphics), he helped build one of the first industrially successful assertion-based verification tool-sets for hardware. He is an ACM Distinguished Scientist.<\/div>\n<\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-7{width:80% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-7 > .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-7{width:80% !important;order : 0;}.fusion-builder-column-7 > .fusion-column-wrapper {margin-right : 2.4%;margin-left : 2.4%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-7{width:100% !important;order : 0;}.fusion-builder-column-7 > .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-5{ 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-6 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-8 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-6\"><hr \/>\n<\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-8{width:100% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-8 > .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-8{width:100% !important;order : 0;}.fusion-builder-column-8 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-8{width:100% !important;order : 0;}.fusion-builder-column-8 > .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-6{ 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-7 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-9 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-4 hover-type-none\"><img width=\"150\" height=\"150\" title=\"AssiaEcole-e1373617327465-802x1024\" src=\"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-content\/uploads\/2021\/03\/AssiaEcole-e1373617327465-802x1024-1-150x150.jpg\" class=\"img-responsive wp-image-1032\"\/><\/span><\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-9{width:20% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-9 > .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-9{width:20% !important;order : 0;}.fusion-builder-column-9 > .fusion-column-wrapper {margin-right : 9.6%;margin-left : 9.6%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-9{width:100% !important;order : 0;}.fusion-builder-column-9 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-10 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-7\"><div><strong>Name<\/strong>: Assia Mahboubi<\/div>\n<div><strong>Title<\/strong>: <em>Formal verification of computational mathematics<\/em><\/div>\n<div style=\"text-align: justify;\"><strong>Abstract<\/strong>: Computers have changed the practice of research in mathematics, even in its most abstract fields. Widely used as observation instruments for testing and refining conjectures, they can actually also substantiate actual proof steps. A large class of computer proofs today involve symbolic computations, often produced by computer algebra systems. While these systems have become amazingly efficient, they also tend to exhibit awkward behaviors on seemingly innocuous queries. This talk will discuss the challenges raised by the formal verification of symbolic computation.<\/div>\n<div style=\"text-align: justify;\">\n<div style=\"text-align: justify;\">\n<p><strong>Short Bio<\/strong>: Assia Mahboubi is a tenured researcher (charg\u00e9e de recherche) at\u00a0<a href=\"http:\/\/www.inria.fr\/\">Inria<\/a>, in the\u00a0<a href=\"http:\/\/gallinette.inria.fr\/\">Gallinette<\/a>\u00a0team, Nantes, France. She is also an endowed professor in the\u00a0<a href=\"https:\/\/www.math.vu.nl\/en\/research\/algebra-and-number-theory\/index.aspx\">Algebra and Number Theory<\/a>\u00a0section of the\u00a0<a href=\"http:\/\/www.vu.nl\/\">Vrije Universiteit Amsterdam<\/a>, in the Netherlands. Her research interests revolve around the foundations and formalization of mathematics in type theory and the automated verification of mathematical proofs. In particular, she is interested in the new insights that one often gets on familiar mathematical objects when looking for their most adequate formal representation for the purpose of computer-aided proof checking. She also has a special interest for the interplay between computer algebra and formal proofs, and more generally for computer-aided mathematics. I am a happy, intensive user of the\u00a0<a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a>\u00a0interactive proof assistant, and a lead developer of the\u00a0<a href=\"https:\/\/github.com\/math-comp\/math-comp\">Mathematical Components<\/a>\u00a0libraries.<\/p>\n<\/div>\n<\/div>\n<\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-10{width:80% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-10 > .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-10{width:80% !important;order : 0;}.fusion-builder-column-10 > .fusion-column-wrapper {margin-right : 2.4%;margin-left : 2.4%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-10{width:100% !important;order : 0;}.fusion-builder-column-10 > .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-7{ 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\/1019"}],"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=1019"}],"version-history":[{"count":25,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1019\/revisions"}],"predecessor-version":[{"id":1460,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1019\/revisions\/1460"}],"wp:attachment":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/media?parent=1019"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}