VPT 2014 - Second International Workshop on Verification and Program Transformation

Recent research in both fields has shown a great potential for mutually beneficial interactions. On the one hand the methods, techniques and tools developed in program transformations have been successfully applied for verification of programs, systems and protocols specified by programs. Partial evaluation, partial deduction, fold/unfold transformations, supercompilation and distillation have all been used for verification with a particular success in the verification of infinite-state and parameterized systems. In opposite direction, model checking, automated and interactive theorem proving, SAT- and SMT-based methods have been used to strengthen and optimize program transformations. Yet another area on the border of two fileds, that is formal verification and certification of programs transformations tools, such as automated refactoring tools and compilers has attracted considerable interest, posed major challenges and yielded promising results.
The workshop will provide a forum where all these interactions can be presented and discussed. The workshop will solicit research, position, applications and system description papers with a special emphasis on case studies, demonstrating viability of the interfaces between the two research fields in a broad sense. The papers dealing with neighboring areas, such as testing and program synthesis will be welcomed too.
The workshop will offer twofold benefits for the verification community. On the one hand it will rise awareness of and stimulate the development of novel verification methods and techniques. On the other hand it will draw an attention of the community to the novel and challenging verification problems and research opportunities.