Invited Speaker: Manuel Fähndrich, Microsoft Research
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.
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
languages (e.g., functional, imperative, object-oriented), and apply to
diverse kinds of program properties (e.g.,
data structure invariants, security properties, temporal protocols).
fall into one of the following three categories:
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
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.
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