The Fifth ACM SIGPLAN Workshop
on
Programming Languages meets Program Verification 


29th January, 2011
Austin, Texas
(Affiliated with POPL 2011)


Overview 

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. Examples include dependently typed programming languages, which leverage a language's type system to specify and check richer than usual specifications, possibly with programmer-provided proof terms, extended static checking systems like ESC/Java and Spec#, which incorporate contracts and static contract verifiers.

We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. To encourage cross-pollination between different communities, we seek a broad the scope for PLPV.  In particular, submissions may have diverse foundations for verification (Type-based, Hoare-logic-based, Abstract Interpretation-based, 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).



Important Dates

Submission 11th October, 2010
Notification 8th November, 2010
Final Version 15th November, 2010
Workshop 29th January, 2011


Submissions

Submissions should fall into one of the following categories:

Research papers (12 pages) that describe new work on the above or related topics. Submissions in this category have an upper limit of 12 pages but shorter submissions are also encouraged. 

Proposals for challenge problems (6 pages) which the author believes are useful benchmarks or important domains for language-based program verification techniques.  Submissions in this category should be at most 6 pages in total length.

Submissions should be prepared with
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.


Publication

Accepted papers will be published by the ACM and will appear in the ACM Digital library. The authors of selected papers will be invited to submit an extended version of their paper to a special issue of the Journal of Formalized Reasoning devoted to papers from PLPV 2011.


Student Attendees

Students with accepted papers or posters are encouraged to apply for a SIGPLAN PAC grant that will help to cover travel expenses to PLPV. Details on the PAC program and the application can be found here. PAC also offers support for companion travel.