Programming Languages meets Program Verification (PLPV)

Topic. The PLPV workshop is concerned with language-based approaches to program verification. These approaches integrate programming language semantics and verification techniques in a tighter way than is typically done in traditional verification. An example is dependently typed programming, where types provide rich specifications, and programs may contain proof terms to establish type equivalences or satisfy pre-conditions. The motivation for this approach is to reduce the burden of program verification by taking greater advantage of semantic properties (like type properties) of the program during verification.

Meetings of PLPV: Steering Committee, 2011-2014.
Former Steering Committee, 2007-2010.