| 日時(Date) |
2026年01月09日 (金) / Jan. 09th, 2026 (Fri.) 3限 (13:30--15:00) / 3rd period (13:30--15:00) |
|---|---|
| 場所(Location) | online (Meeting link) |
| 司会(Chair) | Shimari sensei |
| 講演者(Presenter) | AFFELDT Reynald and 川本 裕輔(客員教授 and 客員准教授, 国立研究開発法人産業技術総合研究所) |
| 題目(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 Rocq proof assistant. |
| 講演言語(Language) | English/Japanese |
| 講演者紹介(Introduction of Lecturer) | ** |