More Third-Party Tools

SyGuS

SyGuS solvers for invariant synthesis/generation:

• CVC5 (github repository)

  An open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

• LoopInvGen (github repository)

  A data-driven tool that generates provably sufficient loop invariants for program verification.

• DryadSynth (github repository)

  A SyGuS solver that reconciles enumerative and deductive program synthesis.

Non-linear Invariant

• PolyHorn (github repository)

  Supports CHC frontend for non-linear invariant generation.