Programming Languages meets Program Verification (PLPV) 2007

October 5, 2007
Freiburg, Germany
Affiliated with ICFP 2007.


Proceedings online at the ACM Digital Library.

Workshop schedule (including unofficial copies of some of the papers).

Invited Speaker: Claude Marché (INRIA)

Topic. PLPV is concerned with language-based approaches to program verification. These approaches integrate programming language semantics and verification techniques in a tighter way than is typically done in traditional verification. An example is dependently typed programming, where types provide rich specifications, and programs may contain proof terms to establish type equivalences or satisfy pre-conditions. The motivation for this approach is to reduce the burden of program verification by taking greater advantage of semantic properties (like type properties) of the program during verification.

Paper Topics. Research on language-based approaches to program correctness spans compilers, programming languages, and computational logic. Possible paper topics include:
Submissions. Submissions should be prepared with ACM SIGPLAN two-column conference format. We request authors to follow the "author-date" citation format which is being used by ICFP. See the ICFP call for papers for more information on this format. 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 (not currently submitted elsewhere for publication).
  2. Work-in-progress reports (at most 6 pages in total length). Submissions in this category need not report orignal research. Instead, they are intended to inform others about interesting and significant applications as well as insights gained in the practice of combining programming with verification.
  3. Proposals for challenge problems (at most 6 pages in total length). Submissions in this category should describe an application for which the author believes language-based program verification techniques can be applied to establish correctness. Preference will be given to broadly used applications, and to ones where correctness is of demonstrable importance (a crucial piece of Internet infrastructure might be an example).
Online Submission. Electronic submission of PDF files is now closed (EasyChair page for PLPV07).

Review Process. Each submission will receive three reviews. The PC members (except the co-chairs) may submit either kind of paper. Reviewing (as well as submission) will be managed using the EasyChair system, which prevents PC members from accessing discussions of their own papers.

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

Important Dates (finalized). Organizers. Program Committee.
Previous PLPVs: