Verifying Full Regular Temporal Properties of Programs via Dynamic Program Execution

摘要

Verification of programs at code level has attracted more and more attentions since the cost is high to extract models from source code. Most of approaches available for code level verification are carried out by inserting assertions into programs and the