Synthesis of Circular Compositional Program Proofs via Abduction

Boyang Li, Isil Dillig, Thomas Dillig, Kenneth L. McMillan, and Mooly Sagiv


In this paper, we propose a technique for synthesizing circular compositional

proofs of program correctness. Our technique uses abductive inference to

decompose the proof into small lemmas,

which are represented as small program fragments annotated

with pre and post-conditions. Different

verification tools can be used to discharge each different lemma,

thereby combining the strengths of different verifiers. Furthermore, each

lemma concerns the correctness of small syntactic fragments of the program,

addressing scalability concerns. We have

implemented this technique and used it combine four different

verification tools. Our experiments show that our technique can be

successfully used to verify applications that cannot be verified by any

individual technique.


Publication typeInproceedings
Published in19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
> Publications > Synthesis of Circular Compositional Program Proofs via Abduction