Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition

From MaRDI portal