By John P. Gallagher, Roskilde University, Denmark and IMDEA Software Institute, Madrid, Spain
[email protected]
Abstract:
Specialisation is a program transformation that transforms a program with respect to given constraints that restrict its behaviour. Typically, the goal is to optimise a program, but specialisation can also transform programs to make them more amenable to analysis and verification.
Here, we outline an algorithm for polyvariant specialisation of constrained Horn clauses (CHCs). Using CHCs as a representation language for imperative code, this has led to recent applications of the algorithm in termination and cost analysis, program verification and derivation of sufficient preconditions for program safety.