Verifying Temporal Properties of C Programs via Lazy Abstraction

摘要

To verify both safety and liveness temporal properties of programs in practice, this paper investigates scalable Linear Temporal Logic (LTL) property verification approach of C programs. We show that the verification target can be accomplished as a scalable lazy abstraction supplemented Counter-Example Guided Abstraction Refinement (CEGAR) based program analysis task. As a result, the scalable lazy abstraction based safety property analysis approaches as well as their mature supporting tools can be reused to verify temporal properties of C programs. We have implemented the proposed approach in TPChecker to verify temporal properties of C programs. Experimental results on benchmark programs show that the proposed approach performs well when verifying non-safety temporal properties of C programs.