Symbolic Execution and Deductive Verification Approaches to VerifyThis 2017 Challenges

摘要

We present solutions to the VerifyThis 2017 program verification challenges using the symbolic execution tool CIVL. Comparing these to existing solutions using deductive verification tools such as Why3 and KeY, we analyze the advantages and disadvantages of the two approaches. The issues include scalability; the ability to handle challenging programming language constructs, such as expressions with side-effects, pointers, and concurrency; the ability to specify complex properties; and usability and automation. We conclude with a presentation of a new CIVL feature that attempts to bridge the gap between the two approaches by allowing a user to incorporate loop invariants incrementally into a symbolic execution framework.