VPT 2014
Second International Workshop on
Verification and Program Transformation
as an event of the Vienna Summer of Logic 2014
July 17th and 18th, 2014, Vienna, Austria
Co-Located with the 26th International Conference on Computer Aided Verification


The workshop aims to bring together researchers working in two different areas, Verification and Program Transformation.

The previous workshop in this series was VPT 2013, Saint Petersburg, Russia.

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

Programme

Proceedings


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)
  • Irina A. Lomazova, National Research University Higher School of Economics, Russia
  • Andrei P. Nemytykh, Program Systems Institute of RAS, Russia (co-chair)
  • Johan Nordlander, Chalmers University of Technology, Sweden
  • Alberto Pettorossi, Università di Roma Tor Vergata and
                                 Istituto di Analisi dei Sistemi ed Informatica "A. Ruberti", Italy
  • Sven Schewe, The University of Liverpool, UK
  • Peter Sestoft, The IT University of Copenhagen, Denmark
  • Morten H. Sørensen, Formalit, Denmark
Steering Committee:
  • Geoff W. Hamilton, Dublin City University, Republic of Ireland
  • Alexei Lisitsa, The University of Liverpool, UK
  • Andrei P. Nemytykh, Program Systems Institute of RAS, Russia
  • Alberto Pettorossi, Università di Roma Tor Vergata and
                                 Istituto di Analisi dei Sistemi ed Informatica "A. Ruberti", Italy
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 30th, 2014: Paper submission deadline
  • April 14th, 2014: Extended paper submission deadline
  • May 15th, 2014: Acceptance notification
  • May 16th, 2014: Acceptance notification
  • May 25th, 2014: Camera ready version
  • June 2nd, 2014: Camera ready version
  • July 17th and 18th, 2014: 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 14th 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.


Contacts
 
a.lisitsa@csc.liv.ac.uk
nemytykh@math.botik.ru