From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p97A24re023808 for ; Fri, 7 Oct 2011 12:02:05 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ai8CAEzNjk7RVdIwk2dsb2JhbABEDqglCCIBAQEBCQkLCRQEIYFsAgkjARsMAw8DEhBaAwERAQUBIxsZh2ObGgqLUIJehQwTKohvAgQGhywEjBiHV40bPYM4OQ X-IronPort-AV: E=Sophos;i="4.68,501,1312149600"; d="scan'208";a="123190266" Received: from mail-pz0-f48.google.com ([209.85.210.48]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 07 Oct 2011 12:01:58 +0200 Received: by mail-pz0-f48.google.com with SMTP id 36so10351951pzk.7 for ; Fri, 07 Oct 2011 03:01:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type :content-transfer-encoding; bh=t7E+ewD0Bur3Zlsn4FZ1rkBxib51GCz0f1Y54+WKOaw=; b=A7OWkO9CkwqYMEDbmAfQG4LVHOQFaXlhvp6MBQz/UjggpBD9eYmutBbmEFDzSRNQBA rXbyObDZ1oasqqwufiv3AElGzE9PzJkoIjnDyk0HfNyaGmLEPpJVWCHkZ1XUUiYHBRCP QlNw7MiUIQFWA6AntgIBw/FGah2cJlm5PidjE= MIME-Version: 1.0 Received: by 10.68.27.199 with SMTP id v7mr13093648pbg.2.1317981718057; Fri, 07 Oct 2011 03:01:58 -0700 (PDT) Received: by 10.68.50.130 with HTTP; Fri, 7 Oct 2011 03:01:57 -0700 (PDT) Date: Fri, 7 Oct 2011 12:01:57 +0200 Message-ID: From: PLPV 2012 To: finite-model-theory@lists.rwth-aachen.de, logic-list@helsinki.fi, spin_list@research.bell-labs.com, theorem-provers@ai.mit.edu, calculemus-ig@ags.uni-sb.de, concurrency@cwi.nl, formal-methods@cs.uidaho.edu, hol-info@lists.sourceforge.net, als+lics-request@inf.ed.ac.uk, metaprl@metaprl.org, pvs@csl.sri.com, acl2@cs.utexas.edu, agda@lists.chalmers.se, isabelle-users@cl.cam.ac.uk, caml-list@inria.fr, clean-list@science.ru.nl, erlang-questions@erlang.org, fp-nl@cs.uu.nl, haskell@haskell.org, plt-scheme@list.cs.brown.edu, prog-lang@diku.dk, seworld@sigsoft.org, sml-list@cs.cmu.edu Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p97A24re023808 X-Validation-by: plpv2012@gmail.com Subject: [Caml-list] 2nd CFP: Programming Languages meets Program Verification (PLPV 2012)                              PLPV 2012                     The Sixth ACM SIGPLAN Workshop            Programming Languages meets Program Verification                      --- 2nd call for papers --- !!! Note: Submission deadline updated to October 14, 2011 !!! 24th January, 2012 Philadelphia, USA (Affiliated with POPL 2012) http://research.microsoft.com/en-us/um/people/nswamy/plpv12 -------------------------------------------------------------------------------- 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. Examples include dependently typed programming languages, which leverage a language's type system to specify and check richer than usual specifications or 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 cross-pollination between different communities, we seek a broad scope for PLPV.  In particular, submissions may have diverse foundations for verification (Type-based, Hoare-logic-based, Abstract Interpretation-based, 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:    14th October,  2011 (extended!) Notification:  8th November,  2011 Final Version: 15th November, 2011 Workshop:      24th January,  2012 -------------------------------------------------------------------------------- Submissions We seek submissions of up to 12 pages related to the above topics---shorter submissions are also welcome. Submissions may describe new work, propose new challenge problems for language-based verification techniques, or present a known idea in an elegant way (i.e., a pearl). Submissions should be prepared with SIGPLAN two-column conference format (http://www.sigplan.org/authorInformation.htm). Submitted papers must adhere to the SIGPLAN republication policy (http://www.sigplan.org/republicationpolicy.htm). Concurrent submissions to other workshops, conferences, journals, or similar forums of publication are not allowed. To submit a paper, access the submission site at http://www.easychair.org/conferences/?conf=plpv2012. -------------------------------------------------------------------------------- Publication Accepted papers will be published by the ACM and will appear in the ACM Digital library. -------------------------------------------------------------------------------- Program Committee Amal Ahmed            Indiana University Lennart Augustsson    Standard Chartered Koen Claessen         Chalmers (co-chair) Martin Giese          University of Oslo Daniel Licata         Carnegie Mellon University Peter Müller          ETH Zurich Aleksandar Nanevski   IMDEA Matthieu Sozeau       INRIA Nikhil Swamy          Microsoft Research (co-chair) David Walker          Princeton University Dana Xu               INRIA -------------------------------------------------------------------------------- Previous PLPVs: http://plpv.org