Please use this identifier to cite or link to this item:
|Title:||Framework for combining analysis and verification||Authors:||Heintze, N.
|Issue Date:||2000||Citation:||Heintze, N.,Jaffar, J.,Voicu, R. (2000). Framework for combining analysis and verification. Conference Record of the Annual ACM Symposium on Principles of Programming Languages : 26-39. ScholarBank@NUS Repository.||Abstract:||We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. Both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. More importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. In other words, our framework explores synergistic interaction between verification and analysis. In this paper, we start with a representation of a program, user assertions, and a given analyzer for the program. The framework we describe induces an algorithm which exploits the assertions and the analyzer to produce a generally more accurate analysis. Further, it has some important features: it is flexible: any number of assertions can be used anywhere; it is open: it can employ an arbitrary analyzer; it is modular: we reason with conditional correctness of assertions; it is incremental: it can be tuned for the accuracy/efficiency tradeoff.||Source Title:||Conference Record of the Annual ACM Symposium on Principles of Programming Languages||URI:||http://scholarbank.nus.edu.sg/handle/10635/40247||ISSN:||07308566|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Mar 31, 2020
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.