Search

We have proved that for any pattern p the tail recursive program model of naive pattern matching may be automatically specialized w.r.t. the pattern p to a specialized version of the so-called KMP-algorithm, using the Higman-Kruskal relation that controls the unfolding/folding. Given an input string, the corresponding residual program finds the first occurrence of p in the string in linear time on the string length. The current state of the automated program specialization art based on unfolding/folding is too weak in order to be able to reproduce the proof, done by hands, of the uniform property above, while it known before that program specialization is sometimes able to produce the KMP-algorithm for a few concrete static patterns., Comment: Pre-proceedings paper presented at the 31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021), Tallinn, Estonia, and Virtual, September 7-8, 2021 (arXiv:2107.10160)

This volume contains a final and revised selection of papers presented at the Seventh International Workshop on Verification and Program Transformation (VPT 2019), which took place in Genova, Italy, on April 2nd, 2019, affiliated with Programming 2019.

This volume contains the proceedings of the Fifth International Workshop on Verification and Program Transformation (VPT 2017). The workshop took place in Uppsala, Sweden, on April 29th, 2017, affiliated with the European Joint Conferences on Theory and Practice of Software (ETAPS). The aim of the VPT workshop series is to provide a forum where people from the areas of program transformation and program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields. Seven papers were presented at the workshop. Additionally, three invited talks were given by Javier Esparza (Technische Universit\"at M\"unchen, Germany), Manuel Hermenegildo (IMDEA Software Institute, Madrid, Spain), and Alexey Khoroshilov (Linux Verification Center, ISPRAS, Moscow, Russia).

This volume contains the papers selected among those which were presented at the 3rd International Workshop on Verification and Program Transformation (VPT 2015) held in London, UK, on April 11th, 2015. Previous editions of the Workshop were held at Saint-Petersburg (Russia) in 2013, and Vienna (Austria) in 2014. Those papers show that methods and tools developed in the field of program transformation such as partial evaluation and fold/unfold transformations, and supercompilation, can be applied in the verification of software systems. They also show how some program verification methods, such as model checking techniques, abstract interpretation, SAT and SMT solving, and automated theorem proving, can be used to enhance program transformation techniques, thereby making these techniques more powerful and useful in practice.