The Fourth ACM SIGPLAN Workshop
on
Programming Languages meets Program
Verification
Tuesday, January 19, 2010
Madrid, Spain
Affiliated with POPL
2010.
Overview: This will be the fourth ACM
SIGPLAN Workshop on Programming Languages meets Program Verification.
The goal of PLPV is to foster and stimulate research at the
intersection of programming languages and program verification. Work
in this area typically attempts to reduce the burden of program
verification by taking advantage of particular semantic and/or
structural properties of the programming language. One example is
dependently typed programming languages, which leverage a language's
type system to specify and check richer than usual specifications,
possibly with programmer-provided proof terms. Another
example is extended static checking systems like ESC/Java and Spec#,
which incorporate pre- and postconditions along with a static
verifier for these contracts.
Call for Papers
Registration: To register for
PLPV'10, follow the link from the POPL 2010 page.
Schedule
Invited Talk (9:00 - 10:00)
CertiCrypt: Formal
Certification of Code-Based Cryptographic Proofs
Gilles Barthe, Madrid Instutite for Advanced Studies
Session 1 (10:30 - 12:00)
Singleton
types
here, Singleton types there, Singleton types everywhere
Stefan Monnier and David Haguenauer
Operating
system
development with ATS
Matthew Danish and Hongwei Xi
Modular
Reasoning
about Invariants over Shared State with Interposed Data
Members
Stephanie Balzer and Thomas Gross
Session 2 (2:00 - 3:00)
Resource
Typing
in Guru
Aaron Stump and Evan Austin
Free
Theorems
for Functional Logic Programs
Jan Christiansen,
Daniel Seidel and Janis Voigtländer
Discussion (3:00 - 3:30)
Status update and discussion of the Trellys Project
Session 3 (4:00 - 5:00)
Arity-generic
datatype-generic
programming
Stephanie Weirich and Chris
Casinghino
Challenge
Benchmarks
for Verification of Real-time Programs
Tomas
Kalibera, Pavel Parizek, Ghaith Haddad, Gary T. Leavens, and Jan Vitek.
Co-Chairs
Program Committee
Previous PLPVs