
Semantics-based generation of verification conditions via program specialization
Keywords: Horn clauses; Program verification; Program specialization; Semantics of programming languages; Software model checking;