Programming Languages meets Program Verification (PLPV) 2006

A workshop affiliated with IJCAR 2006, a FLoC conference.
Seattle, Washington
August 21, 2006

Preproceedings are here. The FLoC page for PLPV '06 is here.

Motivation. 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.

PL and Verification. 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.

Paper Topics. Research on language-based approaches to program correctness spans compilers, programming languages, and computational logic. Possible paper topics include: Submissions. Submissions should either be new research papers, prepared with article format in LaTeX, between 12 and 18 pages in length (not counting appendices, which reviewers will not be asked to review); or else position papers, same format, of no more than 5 pages. Research papers describing preliminary results or work in progress are very welcome. More time for presentation at the workshop may be allotted for a full paper than a position paper. Electronic submission of PostScript or PDF files should be done via the EasyChair page for PLPV.

Review Process. Each submission will receive three reviews. The co-chairs will limit themselves to position papers, while other PC members may submit either kind of paper. Reviewing (as well as submission) will be managed using the EasyChair system, which prevents PC members from accessing discussions of their own papers.

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.

Important Dates. Invited Speaker: Peter Dybjer

Organizers. Program Committee.