The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification, by bringing together experts from diverse areas like types, contracts, interactive theorem proving, model checking and program analysis. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic or structural properties of the programming language. One example is provided by dependently typed programming languages, which make it possible to specify and check rich specifications using the languages' type systems. Another example is provided by extended static checking systems, which incorporate contracts with either static or dynamic contract checking.
We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. To encourage interaction between different communities, we seek a broad scope for PLPV. In particular, submissions may have diverse foundations for verification (based on types, Hoare-logic, abstract interpretation, etc.), target different kinds of programming languages (functional, imperative, object-oriented, etc.), and apply to diverse kinds of program properties (data structure invariants, security properties, temporal protocols, resource constraints, etc.).
We seek submissions of up to 12 pages related to the above topics; shorter submissions are also welcome. Submissions may describe new work, propose new challenge problems for language-based verification techniques, or present a known idea in an elegant way (as in a pearl).
Submissions should be prepared using the SIGPLAN two-column conference format. Submitted papers must adhere to the SIGPLAN republication policy; concurrent submissions to other workshops, conferences, journals, or similar forums of publication are not allowed. Plagiarism is not allowed, see ACM's plagiarism policy.
Authors of accepted papers are expected to transfer copyright to the ACM, or to give ACM publication rights. Several options are available.
Authors have the option to include auxiliary material with their submissions, but reviewers are not obliged to take such material into account. Authors of accepted papers have the option to publish auxiliary material together with their papers (if they give the ACM publishing rights for this material).
To submit a paper, access the submission site.
Authors take note: All accepted papers will be available from the ACM Digital Library two weeks prior to the workshop, starting from January 7, 2014. The official publication date is the date the proceedings are made available in the ACM Digital Library. The official publication date may affect the deadline for any patent filings related to published work.