Interpolation in practical formal development (Q2716926)

The authors indicate the importance of the presence of interpolants in the logic for expressing specifications of software. They recall some results linking interpolation to important properties such as presentation modularity and proof decomposition. They explain the role of interpolants and modularization for promoting property enrichment from subsystems to systems and for controlling interference. They also advocate the need of reengineering specification logics so that special kinds of interpolants, called uniform interpolants, become available.