ACM SIGPLAN Workshop
Programming Languages meets Program
Tuesday, January 19, 2010
Affiliated with POPL
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 is
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 is extended static checking systems like ESC/Java and Spec#,
which incorporate 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. To encourage cross-pollination between different
communities, we seek a broad the scope for PLPV. In particular,
may have diverse foundations for verification (type-based,
Hoare-logic-based, etc), target diverse kinds of
languages (functional, imperative, object-oriented, etc), and apply to
diverse kinds of program properties (data structure invariants,
security properties, temporal protocols, etc).
submission: 10 October, 2009
- Notification: November 8, 2009
version: November 15, 2009
- Workshop: January 19, 2010
fall into one of the following three categories:
Submissions should be
prepared with SIGPLAN
Submitted papers must adhere to the SIGPLAN
Concurrent submissions to other workshops, conferences, journals,
or similar forums of publication are not allowed.
- Regular research papers 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.
- Work-in-progress reports should describe new work that is
and may not be fully completed or evaluated. Submissions in this
category should be at most 6 pages in total
- Proposals for challenge problems which the author believes is
are useful benchmarks or important
domains for language-based program verification techniques.
Submissions in this category should be at most 6 pages in total
Publication: Accepted papers will be
published by the ACM and appear in the ACM digital library.
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.