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
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
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
Download fromView all 3 versions
e-Prints Soton
Conference object . 2002
Part of book or chapter of book
Provider: UnpayWall
Part of book or chapter of book . 2007
Provider: Crossref
Any information missing or wrong?Report an Issue