[TYPES/announce] CFP: PLPV'12 - Programming languages meets program verification

Nikhil Swamy nswamy at microsoft.com
Tue Sep 6 12:04:08 EDT 2011

                               PLPV 2012
                     The Sixth ACM SIGPLAN Workshop 
            Programming Languages meets Program Verification 

24th January, 2012
Philadelphia, USA
(Affiliated with POPL 2012)


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:    11th October,  2011  
Notification:  8th November,  2011  
Final Version: 15th November, 2011  
Workshop:      24th January,  2012  


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 


Accepted papers will be published by the ACM and will appear in the
ACM Digital library.

Program Committee 

Amal Ahmed            Northeastern 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

More information about the Types-announce mailing list