VPT 2013
First International Workshop on
Verification and Program Transformation
July 13th and 14th, 2013, Saint Petersburg, Russia
Co-Located with the 25th International Conference on Computer Aided Verification

The workshop aims to bring together researchers working in two different areas, 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.

Call for Papers



Invited Speakers: Programme Committee:
  • Maurice Bruynooghe, Katholieke Universiteit Leuven, Belgium
  • Geoff W. Hamilton, Dublin City University, Republic of Ireland
  • Boris Konev, The University of Liverpool, UK
  • Alexei Lisitsa, The University of Liverpool, UK (co-chair)
  • Andrei P. Nemytykh, Program Systems Institute of RAS, Russia (co-chair)
  • Johan Nordlander, Luleå University of Technology, Sweden
  • Sven Schewe, The University of Liverpool, UK
  • Peter Sestoft, The IT University of Copenhagen, Denmark
  • Morten H. Sørensen, Formalit, Denmark
  • Simon Thompson, University of Kent, UK
Topics of Interest
include, but are not limited to:
  • Verification by Program Transformation
  • Verification Techniques in Program Transformation and Synthesis
  • Verification and Certification of Programs Transformations
  • Program Analysis and Transformation
  • Program Testing and Transformation
  • Case studies
Important Dates:
  • March 20th, 2013: Visa invitation letters through CAV deadline
  • April 2nd, 2013: Paper submission deadline
  • April 15th, 2013: Extended paper submission deadline
  • May 18th, 2013: Acceptance notification
  • June 3rd, 2013: Camera ready version
  • July 13th and 14th, 2013: Workshop

Proceedings & Submission Guidelines

Regular papers (max. 16 pages) and tool papers (max. 7 pages) must be original and unpublished. Presentations of work-in-progress and relevant but already published work are accepted.

Regular and tool papers accepted for presentation at the workshop will appear in the EasyChair Proceedings in Computing (EPiC) series; they must be prepared in LaTeX using the EasyChair class style and submitted as a single zip file containg both the source of your article and PDF file by 2nd April. The source must contain all auxiliary files required to create the PDF file of your article: this includes images, bibliography, and all non-standard LaTeX packages you used.

Submission accepted for presentation must be presented at the workshop by at least one of the authors.

If the Workshop will attract sufficiently many high quality papers, a special issue of a journal on the topic of the workshop will be considered.


Confirmed Sponsors
                                             RFFI                   CNRS logo                   Rus Acad Sci