DC Field | Value | Language |
---|---|---|
dc.contributor.author | Seo, SN | ko |
dc.contributor.author | Yang, Hongseok | ko |
dc.contributor.author | Yi, Kwangkeun | ko |
dc.date.accessioned | 2017-08-08T06:54:58Z | - |
dc.date.available | 2017-08-08T06:54:58Z | - |
dc.date.created | 2017-08-02 | - |
dc.date.created | 2017-08-02 | - |
dc.date.created | 2017-08-02 | - |
dc.date.issued | 2003 | - |
dc.identifier.citation | PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, v.2895, pp.230 - 245 | - |
dc.identifier.issn | 0302-9743 | - |
dc.identifier.uri | http://hdl.handle.net/10203/225303 | - |
dc.description.abstract | By combining program logic and static analysis, we present an automatic approach to construct program proofs to be used in Proof-Carrying Code. We use Hoare logic in representing the proofs of program properties, and the abstract interpretation in computing the program properties. This combination automatizes proof construction; an abstract interpretation automatically estimates program properties (approximate invariants) of our interest, and our proof-construction method constructs a Hoare-proof for those approximate invariants. The proof-checking side (code consumer's side) is insensitive to a specific static analysis; the assertions in the Hoare proofs are always first-order logic formulas for integers, into which we first compile the abstract interpreters' results. Both the property-compilation and the proof construction refer to the standard safety conditions that are prescribed in the abstract interpretation framework. We demonstrate this approach for a simple imperative language with an example property being the integer ranges of program variables. We prove the correctness of our approach, and analyze the size complexity of the generated proofs. | - |
dc.language | English | - |
dc.publisher | SPRINGER-VERLAG BERLIN | - |
dc.title | Automatic construction of hoare proofs from abstract interpretation results | - |
dc.type | Article | - |
dc.identifier.wosid | 000187786700016 | - |
dc.identifier.scopusid | 2-s2.0-0344152274 | - |
dc.type.rims | ART | - |
dc.citation.volume | 2895 | - |
dc.citation.beginningpage | 230 | - |
dc.citation.endingpage | 245 | - |
dc.citation.publicationname | PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS | - |
dc.contributor.localauthor | Yang, Hongseok | - |
dc.contributor.nonIdAuthor | Seo, SN | - |
dc.contributor.nonIdAuthor | Yi, Kwangkeun | - |
dc.description.isOpenAccess | N | - |
dc.type.journalArticle | Article; Proceedings Paper | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.