Bibliographic Details
| Title: |
Verifying Programs Using Abstraction and Theorem Proving. |
| Authors: |
Junyan Qian1 qjy2000@gliet.edu.cn, Baowen Xu2 bwxu@seu.edu.cn |
| Source: |
International MultiConference of Engineers & Computer Scientists 2007 (Volume 1). 2007, p1044-1049. 6p. 1 Chart. |
| Subjects: |
Automatic theorem proving, Abstract thought, Software verification, Parallel computer program verification, Computer software |
| Abstract: |
We present a methodology for automatically verifying programs against safety specifications based on finite state machine. Firstly, computing the abstract transition between abstract states is done by calling a theorem prover, and then an initial abstract model automatically is extracted from concrete program using predicate abstraction. However, the process of abstraction can be exponential in the number of predicates used. Program slicing, predicate inference and partitioning the set of candidate predicates into subsets make abstract model construction effective. By counterexample-guided abstraction refinement scheme, the abstraction refines incrementally until the specification is either satisfied or refuted. Finally, our methods can be extended to verifying concurrency programs by parallel composition. [ABSTRACT FROM AUTHOR] |
|
Copyright of International MultiConference of Engineers & Computer Scientists 2007 (Volume 1) is the property of International Association of Engineers (IAENG) and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
