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...

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Martin C. Rinard
• Keywords: Automated Reasoning, CADE 2009, Multiple Automated Reasoning, Powerful Automated Reasoning, Reasoning Systems