Sound up-to techniques and Complete abstract domains
Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, Duško Pavlović · 2018
Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been introduced as enhancements of coinduction, an abstract principle to prove properties expressed via greatest fixed-points.