{"id":1793,"date":"2012-08-31T10:00:00","date_gmt":"2012-08-31T10:00:00","guid":{"rendered":"https:\/\/blogs.msdn.microsoft.com\/msr_er\/2012\/08\/31\/workshop-explores-opportunities-in-verified-software\/"},"modified":"2016-07-20T07:32:36","modified_gmt":"2016-07-20T14:32:36","slug":"workshop-explores-opportunities-in-verified-software","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/workshop-explores-opportunities-in-verified-software\/","title":{"rendered":"Workshop Explores Opportunities in Verified Software"},"content":{"rendered":"

Building verifiably reliable and trustworthy software is one of the ultimate objectives of software engineering. With this goal in mind, academics, scientists, and researchers gathered in Shanghai, China, for the second Verified Software Workshop and Summer School (opens in new tab)<\/span><\/a>. The event, which took place from August 23 to 31, 2012, attracted approximately 250 faculty and student attendees from more than 70 universities and research institutes and nearly a dozen countries across the Asia Pacific region and beyond.<\/span><\/p>\n

\"World-class
World-class scientists and researchers—from Asia, Europe, and North America—provided the latest insights into verification theory, practice, and tools.<\/span><\/span><\/p>\n

Co-sponsored by Microsoft Research Asia (opens in new tab)<\/span><\/a> and East China Normal University (opens in new tab)<\/span><\/a>, the event explored new directions and emerging opportunities in verified software research, with 21 keynote presentations by world-class scientists and researchers—from Asia, Europe, and North America—providing the latest insights into verification theory, practice, and tools. Especially notable among the prominent presenters were the workshop co-chairs: Professor Tony Hoare (opens in new tab)<\/span><\/a>, the 1980 Turing Award winner and a principal researcher at Microsoft Research Cambridge (opens in new tab)<\/span><\/a>, who gave the opening speech, titled, “Algebra Unifies Theories of Programming”; and Professor Jifeng He (opens in new tab)<\/span><\/a> of East China Normal University and a member of the of the Chinese Academy of Sciences (opens in new tab)<\/span><\/a>, who delivered a keynote on “A Clock-Based Framework for Modeling Hybrid Systems.”<\/span><\/p>\n

The event began with a two-day workshop at East China Normal University that included inspiring lectures from technical and academic leaders. A broad and comprehensive workshop, it featured in-depth talks on such topics as detection of concurrency bugs, safe programming of asynchronous interaction, pervasive model checking, analysis and verification of multiple programs, automation of program verification, concurrent software verification, software analytics and its application, and modeling and verification of hybrid systems. <\/span><\/p>\n

A five-day summer school of intense training followed the workshop. Students were treated to lectures focusing on the theoretical nature of concurrency and separation logic. One particular highlight was the hybrid systems session, which taught the KeYmaera logical analysis approach in a single day’s time. In addition, a step-by-step tool session provided attendees with valuable hands-on practice and an in-depth learning experience.<\/span><\/p>\n

The event was popular with both students and presenters. Summing up the benefits of the event, one student said, “I acquired cutting-edge research and tools in [the] verification software field, and also had the opportunity to exchange my ideas with innovative peers and academic leads from across the world.”<\/span><\/p>\n

Capturing the perspective of the experienced researcher, co-chair Tony Hoare praised the event and laid out his goals for such venues, saying, “We hope to expand the opportunities for industrial application of mature academic research, and to encourage the next generation of advanced researchers to continue the pursuit of deep and interesting questions in areas of the software industry.”<\/span><\/p>\n

\"Professor
Professor Tony Hoare, the 1980 Turing Award winner and a principal researcher at Microsoft Research Cambridge, gave the opening speech, titled, “Algebra Unifies Theories of Programming.”<\/span><\/span><\/p>\n

Co-chair Jifeng He added, “We have achieved a lot in [the] verified software field with everyone’s great effort, but there is always more work to do. With this event, we hoped to not only inspire our young talent but also provide researchers and faculties worldwide with the advantage of exchanging ideas.”<\/span><\/p>\n

Lolan Song (opens in new tab)<\/span><\/a>, the senior director of Microsoft Research Asia, spoke of the company’s objectives in sponsoring such events, observing that “We hold this event in order to advance the state of the art in software and present a great opportunity for academics, researchers, and students in this area to share and exchange ideas. Also, we hope to identify and cultivate worldwide top talent in verified software areas and build up cadres of experienced users to support eventual use of the tools in the industry.” She also expressed the gratitude of Microsoft Research Asia for the assistance and participation of colleagues from Microsoft Research Cambridge (opens in new tab)<\/span><\/a>, Microsoft Research Redmond (opens in new tab)<\/span><\/a>, and Microsoft Research India (opens in new tab)<\/span><\/a>.<\/span><\/p>\n

—Kangping Liu, University Relations Manager, Microsoft Research Connections Asia<\/span><\/em><\/p>\n

Learn More<\/span><\/strong><\/p>\n