ADVANCED HIGH-ASSURANCE SOFTWARE TECHNOLOGY BY PROOF ASSISTANTS WITH HIGHER-ORDER REWRITING


France-Japan Sakura 2022-2023 project

Participants:

Scientific objective: As information systems have become one of the important social infrastructures, the security assurance of software has become a major issue. However, computer software is very difficult to construct and to guarantee its security. In order to provide a high level of reliability assurance for software in general, rather than for each individual problem, it is necessary to have software technology that is widely applicable and based on rigorous theory. The purpose of this project is to develop and apply an automatic theorem proving system for safety assurance technology for software, and to realize the advancement of software safety assurance technology. In order to achieve this goal, we aim to develop a theorem proving system as a basic theory to realize a highly functional theorem proving system. Specifically, the following topics will be studied:

News:


Statcounter W3C Validator Last updated on 1 December 2022. Come back to main page.