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.


Session 1: 9:00am-10:00am    (Chair: Dana Xu)
   LTL types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional
   Reactive Programs
   Alan Jeffrey

   A Hoare Calculus for the Verification of Synchronous Languages
   Manuel Gesell and Klaus Schneider

Session 2: 10:30am-12:00pm    (Chair: Nikhil Swamy)
   Invited talk: Could We Verify an Information-flow Computer?
   Benjamin C. Pierce
   University of Pennsylvania

Session 3: 2:00pm-3:30pm    (Chair: Matthieu Sozeau)
   Reflexive Toolbox for Regular Expression Matching
   Vladimir Komendantsky

   Formal Network Packet Processing with Minimal Fuss: Invertible Syntax Descriptions at Work
   Reynald Affeldt, David Nowak and Yutaka Oiwa

   The VerCors project - setting up basecamp
   Afshin Amighi, Stefan Blom, Marieke Huisman and Marina Zaharieva-Stojanovski

Session 4: 4:00pm-5:00pm   (Chair: Amal Ahmed)
   Dependent Interoperability
   Peter-Michael Osera, Vilhelm Sjoberg and Steve Zdancewic.

   Equational Reasoning about Programs with General Recursion and Call-by-value Semantics
   Garrin Kimmell, Aaron Stump, Harley Eades, Peng Fu, Tim Sheard, Stephanie Weirich,
   Chris Casinghino, Vilhelm Sjoberg, Nathan Collins and Ki Yung Ahn

The proceedings will be available in the ACM digital library.

Student Attendees
Students with accepted papers or posters are encouraged to apply for a SIGPLAN PAC grant that will help to cover travel expenses to PLPV. Details on the PAC program and the application can be found here.

Program committee

PLPV 2012: Call for papers

Previous PLPVs