Home

Effective Interactive Proofs for Higher-Order Imperative Programs

Effective Interactive Proofs for Higher-Order Imperative Programs

We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification.

Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules.

We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure verification, our system includes much less code that must be trusted; namely, about a hundred lines of Coq code defining a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from first principles, removing opportunities for tool bugs to create faulty verifications.

Adam Chlipala has been telling us how underutilized Coq's Ltac tactic programming language for proof automation is for years. Here is the... er... proof.

By Paul Snively at 2009-08-06 16:54 | Implementation | Software Engineering | Type Theory | other blogs | 10784 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Ltac

Interesting comment on ltac. Never heard of it before - but I've also never used Coq.

Apparently you are one of the only people on LtU to discuss it.

The design of strategy languages is something that interests me. I especially love Manuel Clavel's breakdown of them into his taxonomy, contrasting LCF family languages to Maude.

By Z-Bo at Thu, 2009-08-06 21:11 | login or register to post comments

Where

Where can I read his taxonomy?

By Vilhelm Sjoberg at Mon, 2009-08-10 18:55 | login or register to post comments

In his Ph.D. thesis

Vilhelm,

I just saw your post today. Sorry for the long delay.

Manuel Clavel published his Ph.D. thesis as a magnificient book that is a tour de force of mathematical reasoning using reflection. His book is titled Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications (ISBN-10: 1575862379; ISBN-13: 978-1575862378). He covers the initial contrast in the first chapter, but the rest of the book outlines the contrast.

You may want to learn Maude to make full use of the rest of the book. However, if you work at a large institution (university or company with large R&D/operations branch), you could probably request it ordered. It appears used copies of his book are presently available at reasonable prices ($20). There is really only one book for learning Maude for beginners. All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic (ISBN-10: 3540719407; ISBN-13: 978-3540719403).

By Z-Bo at Mon, 2010-02-01 03:18 | login or register to post comments