PLPV 2010

ACM SIGPLAN Workshop
on
Programming Languages meets Program Verification

PLPV 2010

Tuesday, January 19, 2010
Madrid, Spain
Affiliated with POPL 2010.

Important Dates

Electronic submission: 10 October, 2009
Notification: November 8, 2009
Final version: November 15, 2009
Workshop: January 19, 2010

Accepted Papers

Challenge Benchmarks for Veriﬁcation of Real-time Programs. By Tomas Kalibera, Gary Leavens and Jan Vitek.
Arity-generic datatype-generic programming. By Stephanie Weirich and Chris Casinghino.
Free Theorems for Functional Logic Programs. By Jan Christiansen, Daniel Seidel and Janis Voigtländer.
Singleton types here, Singleton types there, Singleton types everywhere. By Stefan Monnier and David Haguenauer.
Operating system development with ATS. By Matthew Danish and Hongwei Xi.
Resource Typing in Guru. By Aaron Stump and Evan Austin.
Modular Reasoning about Invariants over Shared State with Interposed Data Members. By Stephanie Balzer and Thomas Gross.

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 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, submissions may have diverse foundations for verification (type-based, Hoare-logic-based, etc), target diverse kinds of programming languages (functional, imperative, object-oriented, etc), and apply to diverse kinds of program properties (data structure invariants, security properties, temporal protocols, etc).

Submissions

Submissions should fall into one of the following three categories:

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 ongoing and may not be fully completed or evaluated. Submissions in this category should be at most 6 pages in total length.
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 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 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.

Co-Chairs

Cormac Flanagan (University of California, Santa Cruz)
Jean-Christophe Filliâtre (CNRS)

Program Committee

Adam Chlipala (Harvard University)
Ranjit Jhala (University of California, San Diego)
Joseph Kiniry (University College Dublin)
Rustan Leino (Microsoft Research)
Xavier Leroy (INRIA Paris-Rocquencourt)
Conor McBride (University of Strathclyde)
Andrey Rybalchenko (Max Planck Institute for Software Systems)
Tim Sheard (Portland State University)
Stephanie Weirich (University of Pennsylvania)

Previous PLPVs