| Budget Amount *help |
¥17,940,000 (Direct Cost: ¥13,800,000、Indirect Cost: ¥4,140,000)
Fiscal Year 2021: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2020: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2019: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2018: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2017: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
|
|---|
| Outline of Final Research Achievements |
We have achieved the following research results. (1) New methods for temporal property verification of higher-order programs. (2) New results on cyclic proof systems,formal deduction systems for mathematical induction, and new methods for deciding validity of formulas in first-order fixpoint logic with background theories. (3) A new type and effect system for verifying temporal properties of programs with algebraic effects and handlers, an emerging programming language feature for uniformly expressing a variety of computational effects including destructive updates. (4) Research achievements on the application of program verification and synthesis techniques to security, such as a method for repairing real-world regular expressions vulnerable to ReDoS attacks. (5) New results on the formal language theory of regular expressions extended with real-world features such as backreferences and lookaheads.
|
