Please use this identifier to cite or link to this item:
DC FieldValue
dc.titleFramework for combining analysis and verification
dc.contributor.authorHeintze, N.
dc.contributor.authorJaffar, J.
dc.contributor.authorVoicu, R.
dc.identifier.citationHeintze, 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.
dc.description.abstractWe 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.
dc.typeConference Paper
dc.contributor.departmentCOMPUTER SCIENCE
dc.description.sourcetitleConference Record of the Annual ACM Symposium on Principles of Programming Languages
Appears in Collections:Staff Publications

Show simple item record
Files in This Item:
There are no files associated with this item.

Page view(s)

checked on Mar 22, 2020

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.