FiB: Squeezing loop invariants by interpolation between forward/backward predicate transformers | Publicación