Show simple item record

AuthorDold, Axeldc.contributor.author
AuthorHenke, Friedrich Wilhelm vondc.contributor.author
AuthorVialard, Vincentdc.contributor.author
AuthorGoerigk, Wolfgangdc.contributor.author
Date of accession2016-03-14T13:38:40Zdc.date.accessioned
Available in OPARU since2016-03-14T13:38:40Zdc.date.available
Year of creation2002dc.date.created
AbstractWe report on a large verification effort in constructing an initial fully trusted bootstrap compiler executable for a realistic system programming language and real target processor. The construction and verification process comprises three tasks: the verification of the compiling specification (a relation between abstract source and target programs) with respect to the language semantics and a realistic correctness criterion. Second, the implementation of this specification in the high-level source language following a transformational approach, and third, the construction of a binary executable written in the compilers target language. The focus of this report is on the first verification task. This proof has been completely mechanized using the PVS specification and verification system and is one of the largest case-studies in formal verification we are aware of.dc.description.abstract
Languageendc.language.iso
PublisherUniversität Ulmdc.publisher
LicenseStandard (Fassung vom 03.05.2003)dc.rights
Link to license texthttps://oparu.uni-ulm.de/xmlui/license_v1dc.rights.uri
LCSHCompilers (Computer programs)dc.subject.lcsh
TitleA mechanically verified compiling specification for a realistic compilerdc.title
Resource typeArbeitspapierdc.type
DOIhttp://dx.doi.org/10.18725/OPARU-334dc.identifier.doi
URNhttp://nbn-resolving.de/urn:nbn:de:bsz:289-vts-53499dc.identifier.urn
FacultyFakultät für Informatikuulm.affiliationGeneral
Date of activation2005-09-05T14:49:45Zuulm.freischaltungVTS
Peer reviewneinuulm.peerReview
DCMI TypeTextuulm.typeDCMI
VTS-ID5349uulm.vtsID
CategoryPublikationenuulm.category
Ulm seriesUlmer Informatik-Berichteuulm.seriesUlmName


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record