Project
Construction of a formal foundation that supports the verification of physical and probabilistic systems
News
Tags :
All
There is no notice at the moment
Project outline
| PI | Affeldt Reynald |
|---|---|
| Period | 2022-2025 |
| Outline | Today, computer programs, in addition to the manipulation of digital information and their networks, interact with the outside world, for program verification, not only formal logic and discrete mathematics, but also real analysis, probability theory, geometry, etc. Learning is necessary, and it is difficult to rigorously verify the various side effects of the program. To reduce its complexity, both a fundamental study of the semantics of the program and an integrated study that gives a consistent formal expression to advanced mathematics are necessary. In this study, on the theorem proof support system Rocq, real analysis, continuous probability, rigid geometry are formalized, and based on monad and equation reasoning, the formal foundation is constructed and evaluated. |
| Related research groups | Continuum Computing Trustworthiness Research Group |
| External cooperation | Nagoya University, Kyoto Sangyo University, Tohoku University, Kyushu University |
| External WEB site | https://kaken.nii.ac.jp/ja/grant/KAKENHI-PROJECT-22H00520/ |
