SAC/SVT2013 Talk

An Interactive Extension Mechanism for Reusing Verified Programs

Sosuke Moriguchi & Takuo Watanabe
28th ACM Symposium On Applied Computing (SAC 2013), Technical Track on Software Verification and Testing (SVT), Coimbra, Mar. 18-22, 2013.

Abstract

Interactive theorem provers such as Coq are widely used for program verification. However, if one aims to, for example, add a simple feature to an already-verified program, it may require reconstructing the entire proof. In other words, building upon a verified program (a program with its accompanying proofs) while also maintaining its consistency is generally not an easy task.

We propose a novel method to support the extension of verified programs by interactively modifying their definitions and proofs. We introduce ECoq, an extended version of Coq, which is equipped with a mechanism to help extend inductive types. When a type is modified, ECoq locates the corresponding areas requiring modification in the program and its proofs. Unfortunately, however, this can produce spurious modifications that may complicate the extension of large programs. Hence, we also introduce the concept of ``correction candidates,’’ which are used to reduce the number of spurious modifications semi-automatically.

Publication

Sosuke Moriguchi & Takuo Watanabe, An Interactive Extension Mechanism for Reusing Verified Programs, In Proceedings of the 28th Annual ACM Symposium on Applied Computing (SAC 2013), ACM, pp. 1236-1243, Mar., 2013. DOI: 10.1145/2480362.2480594,

The full-text of this paper is available without charge via this page (thanks to ACM Author-Izer Service).