COMBINE: A Tool on Combined Formal Methods for Bindingly Verification

摘要

Theorem proving and model checking are two well-known formal methods emerging recently for software verification. Each of them has its own advantages and disadvantages. As an attempt to combine the verification capabilities of these two methods, in this paper we introduce a verification tool known as COMBINE (Combined fOrmal Methods for BINdingly vErification). Suggested by its name, COMBINE can verify imperative programs in a bindingly manner comprising of two phases: static verification and dynamic verification. In fact, COMBINE has been developed as a published Web-based system currently being used for teaching programming for students at Hochiminh City University of Technology (HCMUT), Vietnam.