Proceedings of the 7th workshop on Programming languages meets program verification

Welcome to Programming Languages meet Program Verification Workshop 2013! This is the 7th workshop in the PLPV series. The PLPV series of workshops are dedicated to the study of language-based approaches to program verification. The goal of these approaches is to support a correct-by-construction style of software development, in which the programming language provides not just a dynamic execution semantics, but also a static verification semantics. The goal of programming is then to produce programs that are not just correct, but also statically verifiable, and hence programming involves writing both code and a proof sketch of why this code meets its specification. While PLPV-style work does not shy away from full correctness of software, one of its distinguishing characteristics is a focus on extending existing programming languages or methodologies to support lightweight verification. A good example is provided by dependently typed languages, which can verify stronger properties than can typically be shown with traditional type systems, without departing very far from traditional programming methods. Such approaches help to make verification a more natural extension of programming, and thus bring it closer to mainstream use. We were very pleased this year to receive a focused group of 10 high quality submissions. Each paper was reviewed by at least 3 reviewers, which included both PC members and external reviewers. We held an electronic PC meeting via Easychair and email over four days and decided to accept 7 submissions. We also invited Edwin Brady as an invited speaker. The program has an exciting diversity of topics of interest to the PLPV community.