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

Synthesizing Certified Code

Michael W. Whalen; Bernd Fischer; Johann Schumann;
Open Access
  • Published: 01 Jan 2002
  • Publisher: Springer Berlin Heidelberg
  • Country: United Kingdom
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...
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
Download fromView all 3 versions
https://eprints.soton.ac.uk/26...
Part of book or chapter of book
Provider: UnpayWall
e-Prints Soton
Conference object . 2002
http://link.springer.com/conte...
Part of book or chapter of book . 2007
Provider: Crossref
Any information missing or wrong?Report an Issue