Loading...
Please wait, while we are loading the content...
Similar Documents
Proceedings of the 2007 workshop on Programming languages meets program verification (PLPV '07)
| Content Provider | ACM Digital Library |
|---|---|
| Editor | Sulzmann, Martin Stump, Aaron Xi, Hongwei Monnier, Stefan |
| Copyright Year | 2007 |
| Abstract | Welcome to PLPV'07! This workshop is dedicated to the study and development of language-based approaches to program verification. The main goal is to unite programming and verification to support creation of statically verified software. While PLPV-style work does not shy away from full correctness of software, one of its distinguishing characteristics is a focus on extending existing programming languages or methodologies to support lightweight verification. A good example is provided by dependently typed languages. In these languages it is often possible to verify stronger properties than can typically be shown with traditional type systems, without departing very far from traditional programming methods. Such approaches promise not only to achieve a tighter integration between verification and programming, but also to make verification a more natural extension of programming, and thus bring it closer to mainstream use. We were very pleased this year to receive a focused group of high quality submissions. We received 8 regular research papers, limited to 12 pages; and 1 work-in-progress report, limited to 6 pages. We also had a submission category for challenge problem proposals, limited to 6 pages, but we but did not receive any submissions in that category. We accepted the work-in-progress submission, and of the 8 regular research papers, we took 6. Each paper received at least three reviews from members of the PC. No PC member chose to utilize external reviewers. The accepted papers cover what we find to be an exciting diversity of topics from uses of monads for verification; to type systems with advanced features such as dependent types, intersection types, and equality types; to uses of types for compilation and low-level code. We were also very glad that Claude Marché accepted our invitation to be the sole invited speaker for PLPV'07. We were eager to have Claude speak at PLPV, based on his expertise on termination checking and verification of heap-manipulating programs. |
| ISBN | 9781595936776 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2007-10-02 |
| Access Restriction | Subscribed |
| Content Type | Text |
| Resource Type | Conference Proceedings |
