Verifying backwards compatibility of object-oriented libraries using Boogie
Yannick Welsch, Arnd Poetzsch‐Heffter · 2012
Proving that a library is backwards compatible to an older version can be challenging, as the internal representation of the libraries might completely differ and the clients of the library are usually unknown. This is especially difficult in the setting of object-oriented programs with complex heaps and callbacks. Mechanical verification is a key success factor to make such proofs practicable.