Colloquium A

日時(Date) 2023年1月10日(火)3限(13:30--15:00)
Tue. Jan. 10th, 2023, 3rd period (13:30--15:00)
場所(Location) Online (Webex link pass: WXfdyWZA343)
司会(Chair) 嶋利
講演者(Presenter) Prof. Reynald Affeldt(National Institute of Advanced Industrial Science and Technology (AIST)/ 国立研究開発法人産業技術総合研究所)
題目(Title) Formal Verification: Overview and Tool Demonstration
概要(Abstract) Formal verification methods are rigorous techniques for checking the correctness of software, hardware, and systems in general. These techniques are implemented by various automated tools that can check with high confidence any system whose specifications can be couched in mathematical terms. They have been successfully applied to produce bug-free computer programs, to design secure cryptographic protocols, to verify advanced mathematics, etc. In this lecture, we give an overview of the field of formal verification and introduce a general-purpose research tool: the Coq proof assistant.
講演言語(Language) 日本語(main)+English
講演者紹介(Introduction of Lecturer)