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.
Program
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
Abstract
The CRASH/SAFE project aims to design a new computer system that
is highly resistant to cyber-attack. It offers a rare opportunity
to rethink the hardware / OS / software stack from a completely
clean slate, unhampered by legacy constraints. We are building
novel hardware, a new high-level programming language, and a suite
of modern operating system services, all embodying fundamental
security principles -- separation of privilege, least privilege,
mutual suspicion, etc. -- down to their very bones. Achieving
these goals demands a co-design methodology in which all system
layers are designed together, with a ruthless insistence on
simplicity, security, and verifiability at every level.
I will describe the current state of the CRASH/SAFE design and
discuss some of the most interesting verification challenges that
it raises.
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.