摘要
INCAPS,a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program's correctness which are supported respectively by the mechanized logics—FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system: the rules,implementation,tactics,forward proof and backward proof.It also gives several typical exam- pies for demonstration of INCAPS' working principle.The achievement to data is that we have now ac- complished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.
INCAPS,a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program's correctness which are supported respectively by the mechanized logics—FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system: the rules,implementation,tactics,forward proof and backward proof.It also gives several typical exam- pies for demonstration of INCAPS' working principle.The achievement to data is that we have now ac- complished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.
基金
This project is supported by the National Natural Science Foundation of China.
