Duality solves Relation Post-Fixed Point problems using Craig interpolation. In can be used, for example, to generate proofs for procedural programs in the form of procedure summaries. Duality is envisioned as a generic engine for program analysis, supporting applications such as automatic verification of sequential, concurrent and functional programs, as well as interactive refinement of manual proofs.
- Kenneth L. McMillan, Lazy Annotation Revisited, no. MSR-TR-2014-65, 16 May 2014
- Kenneth McMillan and Andrey Rybalchenko, Computing Relational Fixed Points using Interpolation, no. MSR-TR-2013-6, 17 January 2013