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.

@inproceedings{luo-siegel:2018:isola,
  author = {Ziqing Luo and Stephen F.\ Siegel},
  title = {Symbolic Execution and Deductive Verification
    Approaches to {V}erify{T}his 2017 Challenges},
  booktitle = {Leveraging Applications of Formal Methods, Verification
               and Validation (ISoLA 2018), Proceedings, Part II:
               Verification},
  editor = {Margaria, Tiziana and Steffen, Bernhard},
  year = {2018},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = {11245},
  pages = {160--178},
  doi = {10.1007/978-3-030-03421-4_12}
}