Invariant synthesis plays a central role in the verification of programs. In this paper, we propose a novel approach to synthesize basic semialgebraic invariants using semidefinite programming (SDP) that combines advantages of both symbolic constraint solving methods and numeric constraint solving methods. The advantages of our approach are threefold: first, it can deal with arbitrary templates as symbolic computation based techniques; second, it uses SDP instead of computationally intensive symbolic subroutines and is therefore efficient enough as other numeric computation based techniques; lastly, there are some (although weaker) theoretical guarantees on its completeness, which previously can only be provided by symbolic computation based techniques.
Download