@inproceedings { 131, title = {Strengthening Properties using Abstraction Refinement }, booktitle = {DATE}, year = {2009}, pages = {1692-1697}, publisher = {ACM}, organization = {ACM}, address = {Nice}, abstract = {

Model Checking is an automated formal method for verifying whether a finite-state system satisfies a user-supplied specification. The usefulness of the verification result depends on how well the specification distinguishes intended from non-intended system behavior. Vacuity is
a notion that helps formalize this distinction in order to improve the user's understanding of why a property is satisfied. The goal of this paper is to expose vacuity in a property in a way that increases our knowledge of the design. Our approach, based on abstraction refinement, computes a maximal set of atomic subformula occurrences that can be strengthened without compromising satisfaction. The result is a shorter and stronger and thus, generally, more valuable property. We quantify the benefits of our technique on a substantial set of circuit benchmarks.

}, URL = {http://www.kroening.com/publications/view-publications-pwk2009-date.html}, author = {Purandare, P and Wahl, T and Kroening, D} }