publication . Conference object . Book . Part of book or chapter of book . 2002

Synthesizing Certified Code

Michael W. Whalen; Bernd Fischer; Johann Schumann;

Open Access English

Published: 01 Jan 2002

Country: United Kingdom

Summary

Abstract

Code certification is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satisfies certain quality properties. These proofs serve as certificates that can be checked independently. Since code certification uses the same underlying technology as program verification, it requires detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding annotations to the code is time-consuming and error-prone. We address this problem by combining code certification with automatic program synthesis. Given a high-level specification, our app...

Persistent Identifiers

doi: 10.1007/3-540-45614-7_25

Subjects

free text keywords: Proof-carrying code, Code coverage, Source code, media_common.quotation_subject, media_common, Redundant code, Code generation, Loop invariant, Program synthesis, Static program analysis, Computer science, Programming language, computer.software_genre, computer

Related Organizations