Programming Languages meets Program Verification (PLPV) 2009
January 20, 2009 Savannah, Georgia, USA Affiliated with POPL 2009.
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:
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.
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
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:
Electronic submission: October 8, 2008, 11:59pm Samoa time (UTC-11) Submission is closed.
Notification: November 8, 2008
Final version: November 17, 2008
Workshop: January 20, 2009
Accepted papers:
Ana Bove, Peter Dybjer and Andrés Sicard-Ramírez. Embedding a Logical Theory of Constructions in Agda
Levent Erkok and John Matthews. Pragmatic equivalence and safety checking in Cryptol
Kenneth Knowles and Cormac Flanagan. Compositional and Decidable Checking for Dependent Contract Types
Daniel R Licata and Robert Harper. Positively Dependent Types
Max Schaefer, Torbjörn Ekman and Oege de Moor. Challenge Proposal: Verification of Refactorings
Tom Schrijvers, Louis-Julien Guillemette and Stefan Monnier. Type Invariants for Haskell
Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller and Timothy Simpson. Verified Programming in Guru
Noam Zeilberger. Refinement types and computational duality
Organizers:
Thorsten Altenkirch (University of Nottingham, UK)
Todd Millstein (University of California, Los Angeles, USA)
Program Committee:
Andreas Abel (University of Munich, Germany)
Thorsten Altenkirch, co-chair (University of Nottingham, UK)
Jeremy Gibbons (University of Oxford, UK)
Robert Harper (Carnegie Mellon University, USA)
K. Rustan M. Leino (Microsoft Research, USA)
Todd Millstein , co-chair (University of California, Los Angeles, USA)
Ulf Norell (Chalmers University, Sweden)
Jeremy Siek (University of Colorado, Boulder, USA)