Verifying Programs Using Abstraction and Theorem Proving.
Saved in:
| 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 |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 25475487 AccessLevel: 6 PubType: Book PubTypeId: book PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Verifying Programs Using Abstraction and Theorem Proving. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Junyan+Qian%22">Junyan Qian</searchLink><relatesTo>1</relatesTo><i> qjy2000@gliet.edu.cn</i><br /><searchLink fieldCode="AR" term="%22Baowen+Xu%22">Baowen Xu</searchLink><relatesTo>2</relatesTo><i> bwxu@seu.edu.cn</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22International+MultiConference+of+Engineers+%26+Computer+Scientists+2007+%28Volume+1%29%22">International MultiConference of Engineers & Computer Scientists 2007 (Volume 1)</searchLink>. 2007, p1044-1049. 6p. 1 Chart. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Automatic+theorem+proving%22">Automatic theorem proving</searchLink><br /><searchLink fieldCode="DE" term="%22Abstract+thought%22">Abstract thought</searchLink><br /><searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22Parallel+computer+program+verification%22">Parallel computer program verification</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software%22">Computer software</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=25475487 |
| RecordInfo | BibRecord: BibEntity: Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 6 StartPage: 1044 Subjects: – SubjectFull: Automatic theorem proving Type: general – SubjectFull: Abstract thought Type: general – SubjectFull: Software verification Type: general – SubjectFull: Parallel computer program verification Type: general – SubjectFull: Computer software Type: general Titles: – TitleFull: Verifying Programs Using Abstraction and Theorem Proving. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Junyan Qian – PersonEntity: Name: NameFull: Baowen Xu IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 01 Text: 2007 Type: published Y: 2007 Identifiers: – Type: isbn-print Value: 9789889867140 Titles: – TitleFull: International MultiConference of Engineers & Computer Scientists 2007 (Volume 1) Type: main |
| ResultId | 1 |
