Synthesizing Certified Code

Posted by Scott_Ruecker on Sep 7, 2006 1:50 AM EDT
University of Southampton
Mail this story
Print this story

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.

Full Story

  Nav
» Read more about: Story Type: News Story

« Return to the newswire homepage

This topic does not have any threads posted yet!

You cannot post until you login.