<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: Times New Roman; font-size: 12pt; color: #000000'><div style="font-family: Times New Roman; font-size: 12pt; color: #000000"><div style="font-family: Times New Roman; font-size: 12pt; color: #000000"><div style="font-family: Times New Roman; font-size: 12pt; color: #000000"><div><span class="Apple-style-span" style="font-size: 15.9722px; ">Apologies for multiple postings.</span></div><div><span class="Apple-style-span" style="font-family: monospace; font-size: medium; "><span class="Apple-style-span" style="font-family: 'Times New Roman'; font-size: 15.9722px; "><div><br></div></span></span></div><div>---------------------------------------------------------------------------</div><div> The Fifth ACM SIGPLAN Workshop</div><div> on</div><div> Programming Languages meets Program Verification </div><div><span class="Apple-style-span" style="font-size: 15.9722px; "><meta charset="utf-8"><span class="Apple-style-span" style="font-size: 15.9722px; "><div>---------------------------------------------------------------------------</div><div><span class="Apple-style-span" style="font-size: 15.9722px; "> http://cseweb.ucsd.edu/plpv11</span></div></span></span></div><div><meta charset="utf-8"><span class="Apple-style-span" style="font-size: 15.9722px; "><div>---------------------------------------------------------------------------</div><div><br></div></span></div><div><br></div><div>29th January, 2011</div><div>Austin, Texas</div><div>Affiliated with POPL 2011</div><div><span class="Apple-style-span" style="font-size: 15.9722px; "><span class="Apple-tab-span" style="white-space: pre; "> </span></span></div><div><span class="Apple-style-span" style="font-size: 15.9722px; "><div><span class="Apple-style-span" style="font-size: 15.9722px; ">Overview </span></div></span></div><div>--------</div><div><br></div><div>The goal of PLPV is to foster and stimulate research at the intersection of </div><div>programming languages and program verification, by bringing together experts </div><div>from diverse areas like types, contracts, interactive theorem proving, </div><div>model checking and program analysis. Work in this area typically attempts to </div><div>reduce the burden of program verification by taking advantage of particular </div><div>semantic or structural properties of the programming language. Examples include</div><div>dependently typed programming languages, which leverage a language's type system </div><div>to specify and check richer than usual specifications, possibly with </div><div>programmer-provided proof terms, extended static checking systems like ESC/Java </div><div>and Spec#, which incorporate contracts and static contract verifiers.</div><div><br></div><div>We invite submissions on all aspects, both theoretical and practical, of the </div><div>integration of programming language and program verification technology. </div><div>To encourage cross-pollination between different communities, we seek a broad </div><div>the scope for PLPV. In particular, submissions may have diverse foundations</div><div>for verification (Type-based, Hoare-logic-based, Abstract Interpretation-based, etc),</div><div>target different kinds of programming languages (functional, imperative, object-oriented, etc), </div><div>and apply to diverse kinds of program properties (data structure invariants,</div><div>security properties, temporal protocols, resource constraints, etc). </div><div><br></div><div>Important Dates</div><div>---------------</div><div>Submission<span class="Apple-tab-span" style="white-space:pre"> </span>11th October, 2010</div><div>Notification<span class="Apple-tab-span" style="white-space:pre"> </span>8th November, 2010</div><div>Final Version<span class="Apple-tab-span" style="white-space:pre"> </span>15th November, 2010</div><div>Workshop<span class="Apple-tab-span" style="white-space:pre"> </span>29th January, 2011</div><div><br></div><div>Program Committee</div><div>-----------------</div><div><br></div><div><div>Andrew Gordon <span class="Apple-tab-span" style="white-space:pre"> </span> (Microsoft Research)</div><div>Chris Hawblitzel <span class="Apple-tab-span" style="white-space:pre"> </span> (Microsoft Research) </div><div>Ranjit Jhala <span class="Apple-tab-span" style="white-space:pre"> </span> (University of California, San Diego, co-chair)</div><div>Viktor Kuncak <span class="Apple-tab-span" style="white-space:pre"> </span> (Ecole Polytechnique Fédérale de Lausanne)</div><div>John Matthews <span class="Apple-tab-span" style="white-space:pre"> </span> (Galois Inc.)</div><div>James McKinna<span class="Apple-tab-span" style="white-space:pre"> </span> (Radboud University)</div><div>Stefan Monnier<span class="Apple-tab-span" style="white-space:pre"> </span> (Université de Montréal)</div><div>Greg Morrisett <span class="Apple-tab-span" style="white-space:pre"> </span> (Harvard University)</div><div>Christine Paulin-Mohring (Université Paris-Sud)</div><div>Wouter Swierstra <span class="Apple-tab-span" style="white-space:pre"> </span> (Vector Fabrics, co-chair)</div><div>Tachio Terauchi <span class="Apple-tab-span" style="white-space:pre"> </span> (Tohoku University)</div></div><div><br></div><div><br></div><div>Submissions </div><div>-----------</div><div><br></div><div>Submissions should fall into one of the following categories:</div><div><br></div><div>(a) Research papers (12 pages) that describe new work on the above or related topics. </div><div>Submissions in this category have an upper limit of 12 pages but shorter submissions</div><div>are also encouraged. </div><div><br></div><div>(b) Proposals for challenge problems (6 pages) which the author believes are useful </div><div>benchmarks or important domains for language-based program verification techniques. </div><div>Submissions in this category should be at most 6 pages in total length.</div><div><br></div><div>Submissions should be prepared with SIGPLAN two-column conference format. </div><div>Submitted papers must adhere to the SIGPLAN republication policy. Concurrent </div><div>submissions to other workshops, conferences, journals, or similar forums of</div><div>publication are not allowed.</div><div><br></div><div>Publication</div><div>-----------</div><div>Accepted papers will be published by the ACM and will appear in the ACM Digital library. </div><div>The authors of selected papers will be invited to submit an extended version of their </div><div>paper to a special issue of the Journal of Formalized Reasoning devoted to papers </div><div>from PLPV 2011.</div><div><br></div><div>Student Attendees</div><div>-----------------</div><div>Students with accepted papers or posters are encouraged to apply for a SIGPLAN PAC grant </div><div>that will help to cover travel expenses to PLPV. Details on the PAC program and the </div><div>application can be found here. PAC also offers support for companion travel.</div></div></div></div></div></body></html>