Programming Languages meets Program Verification (PLPV) 2009

January 20, 2009
Savannah, Georgia, USA
Affiliated with POPL 2009.


Workshop schedule

Invited Speaker: Manuel Fähndrich, Microsoft Research

Overview: The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic and/or structural properties of the programming language. One example are 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. Another example are extended static checking systems like Spec#, which extends C# with pre- and postconditions along with a static verifier for these contracts.

Paper Topics: We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. By co-locating with POPL 2009, we seek to broaden the scope of PLPV. For example, submissions may have diverse foundations for verification (e.g., type-based, Hoare-logic-based), target diverse kinds of programming languages (e.g., functional, imperative, object-oriented), and apply to diverse kinds of program properties (e.g., data structure invariants, security properties, temporal protocols).

Submissions: Submissions should fall into one of the following three categories:
  1. Regular research papers (at most 12 pages in total length). Submissions in this category should describe new work on the above or related topics.

    Please note that the page limit is an upper limit -- shorter submissions are encouraged.

  2. Work-in-progress reports (at most 6 pages in total length). Submissions in this category should describe new work that is ongoing and may not be fully completed or evaluated.
  3. Proposals for challenge problems (at most 6 pages in total length). Submissions in this category should describe an application area which the author believes is a useful benchmark or important domain for language-based program verification techniques.
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. Please use easychair to submit your paper.

Publication: Accepted papers will be published by the ACM and appear in the ACM digital library.

Important Dates: Accepted papers: Organizers: Program Committee:
Previous PLPVs: