Overview

While the essential ideas of program verification have been understood for decades, the practical ability to develop and maintain correct software at a reasonable cost has remained elusive. Approaches based on manually proving extracted verification conditions are often viewed as brittle and burdensome, despite continued advances. Mostly automatic techniques like static analysis and model checking face challenges scaling to rich properties of large systems. Yet, as societies become increasingly dependent on software systems, the need for a practical way to build provably correct software has never been greater.

Recent work is exploring alternative, language-based approaches to program verification. In these approaches, the programming language provides mechanisms which allow the programmer to express, in some way, her knowledge of why her code meets its specification. This knowledge is connected more intimately to the code than is usually the case for theorem proving approaches. One commonly used mechanism is dependent types. Specifications are expressed as types, and the programming language allows proofs of those specifications to be expressed as terms inhabiting those types. Pre- and post-conditions of functions are recorded in their input and return types, and the functions require and produce proofs of those conditions as additional inputs and outputs. One exciting possibility is that languages for programming with proofs may enable developers to target a "continuum of correctness," through varying amounts of effort on specification and verification.

Program

• PLPV program
• PLPV accepted papers
• PLPV pre-proceedings

Invited Talk

• Monday, August 21st, 09:00‑10:00
  Peter Dybjer (Chalmers University of Technology)
  Programming Languages Meet Program Verification [pdf]

Important Dates.

• Final version: July 18.

Publication

The proceedings of the workshop will most likely be archived using ENTCS or as a technical report (online) at one of the organizers' institutions.

Organizers

• Aaron Stump (Washington University in St. Louis)
• Hongwei Xi (Boston University)

Program Committee

• Thorsten Altenkirch (University of Nottingham)
• Hugo Herbelin (Ecole Polytechnique)
• Simon Peyton-Jones (Microsoft Research)
• Randy Pollack (University of Edinburgh)
• Carsten Schuermann (IT University of Copenhagen)
• Zhong Shao (Yale University)
• Tim Sheard (Portland State University)
• Aaron Stump, co-chair (Washington University in St. Louis)
• Hongwei Xi, co-chair (Boston University)