| 日時(Date) |
2024年 1月 23日 (火) / Tue. Jan. 23rd, 2024 3限 (13:30--15:00) / 3rd period (13:30--15:00) |
|---|---|
| 場所(Location) | エーアイ大講義室, AI Inc. Seminar Hall （L1） |
| 司会(Chair) | 柏 |
| 講演者(Presenter) | Reynald AFFELDT, Yusuke Kawamoto (AIST) / AFFELDT Reynald, 川本 裕輔（国立研究開発法人産業技術総合研究所） |
| 題目(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) | 日本語/English |
| 講演者紹介(Introduction of Lecturer) |