Volume •Abstracts •Preface •Authors •Keywords •BibTex Entries

VPT 2014: Volume Information

VPT 2014. Second International Workshop on Verification and Program Transformation

Editors: Alexei Lisitsa and Andrei Nemytykh

EPiC Series in Computing•Volume 28

9 articles•111 pages•Published: July 28, 2014

Papers

Towards Constraint-Solving over Higher-Order Unbounded Datatypes using Formal Methods Tools

Michael Leuschel

1

Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk)

Klaus von Gleissenthall, Andrey Rybalchenko and Santiago Zanella-Béguelin

2

Program Verification using Constraint Handling Rules and Array Constraint Generalizations

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti

3-18

Branching Processes of Conservative Nested Petri Nets

Daniil Frumin and Irina Lomazova

19-35

Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem

Geoff Hamilton and Morten Heine Sørensen

36-51

A Note on Program Specialization. What Syntactical Properties of Residual Programs Can Reveal?

Alexei Lisitsa and Andrei Nemytykh

52-65

On Unfolding for Programs Using Strings as a Data Type

Andrei Nemytykh

66-83

Verification of Multi-Party Ping-Pong Protocols via Program Transformation

Antonina Nepeivoda

84-98

Formal Replay of Translation Validation for Highly Optimised C

99-111

Keyphrases

Constraint Logic Programming, higher-order, Isabelle/HOL, lambda calculus, Markov's normal algorithms, nested Petri nets, Petri nets, ping-pong protocols, prefix grammar, program analysis², program specialization², program transformation³, program verification, supercompilation⁴, termination, Translation Validation, true concurrency, unfolding, unfoldings, verification³, word equations.