Second call for papers: PLPV 2014 Programming Languages meets Program Verification San Diego, CA, USA Co-located with POPL 2014 http://www.cse.chalmers.se/~nad/plpv-2014/ Overview -------- The goal of PLPV is to foster and stimulate research at the intersection of programming languages and program verification, by bringing together experts from diverse areas like types, contracts, interactive theorem proving, model checking and program analysis. Work in this area typically attempts to reduce the burden of program verification by taking advantage of particular semantic or structural properties of the programming language. One example is provided by dependently typed programming languages, which make it possible to specify and check rich specifications using the languages' type systems. Another example is provided by extended static checking systems, which incorporate contracts with either static or dynamic contract checking. We invite submissions on all aspects, both theoretical and practical, of the integration of programming language and program verification technology. To encourage interaction between different communities, we seek a broad scope for PLPV. In particular, submissions may have diverse foundations for verification (based on types, Hoare-logic, abstract interpretation, etc.), target different kinds of programming languages (functional, imperative, object-oriented, etc.), and apply to diverse kinds of program properties (data structure invariants, security properties, temporal protocols, resource constraints, etc.). Important dates --------------- * Submission deadline: 2013-10-09T24:00-12 (midnight at the end of October 9, 2013, UTC-12) * Author notification: November 1, 2013 * Camera-ready papers due: November 17, 2013 * Workshop: January 21, 2014 Submissions ----------- For details about how to format submissions, where to send them, etc., see http://www.cse.chalmers.se/~nad/plpv-2014/call-for-papers.html. Programme committee ------------------- * Adam Chlipala, MIT * Nils Anders Danielsson, University of Gothenburg (co-chair) * Manuel Fähndrich, Microsoft Research * Philipp Haller, Typesafe * Bart Jacobs, Katholieke Universiteit Leuven (co-chair) * Chantal Keller, Aarhus University * Neelakantan R. Krishnaswami, Max Planck Institute for Software Systems * Andres Löh, Well-Typed LLP * Magnus O. Myreen, University of Cambridge * Alexander J. Summers, ETH Zurich