Differential Assertion Checking

Shuvendu Lahiri, Ken McMillan, Rahul Sharma, and Chris Hawblitzel

Abstract

Previous versions of a program can be a powerful enabler for program analysis by defining new relative specifications and making the results of current program analysis more relevant. In this paper, we describe the approach of it differential assertion checking (DAC) for comparing versions of a program with respect to a set of assertions. DAC provides a natural way to write relative specifications over two programs. We introduce a novel modular approach to DAC by reducing it to single program checking that can be accomplished by any program verifier. In particular, we leverage automatic invariant generation to synthesize relative specifications for pairs of loops and procedures. We provide a preliminary evaluation of a prototype implementation within the symdiff tool along two directions (a) soundly verifying bug fixes in the presence of loops and (b) providing a knob for suppressing alarms when checking a new version of a program.

Details

Publication typeInproceedings
Published inFoundations of Software Engineering (FSE'13)
PublisherACM

Previous versions

Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, and Chris Hawblitzel. Differential Assertion Checking, March 2013.

> Publications > Differential Assertion Checking