Instrumenting a weakest precondition calculus for counterexample generation
scientific article; zbMATH DE number 6895327