Sciweavers

Share
CADE
2009
Springer

Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival

11 years 5 months ago
Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival
In recent years researchers have developed a wide range of powerful automated reasoning systems. We have leveraged these systems to build Jahob, a program specification, analysis, and verification system. In contrast to many such systems, which use a monolithic reasoning approach, Jahob provides a general integrated reasoning framework, which enables multiple automated reasoning systems to work together to prove the desired program correctness properties. We have used Jahob to prove the full functional correctness of a collection of linked data structure implementations. The automated reasoning systems are able to automatically perform the vast majority of the reasoning steps required for this verification. But there are some complex verification conditions that they fail to prove. We have therefore developed a proof language, integrated into the underlying imperative Java programming language, that developers can use to control key choice points in the proof search space. Once the dev...
Martin C. Rinard
Added 23 Nov 2009
Updated 23 Nov 2009
Type Conference
Year 2009
Where CADE
Authors Martin C. Rinard
Comments (0)
books