Zur Kurzanzeige

AutorDold, Axeldc.contributor.author
AutorHenke, Friedrich Wilhelm vondc.contributor.author
AutorVialard, Vincentdc.contributor.author
AutorGoerigk, Wolfgangdc.contributor.author
Aufnahmedatum2016-03-14T13:38:40Zdc.date.accessioned
In OPARU verfügbar seit2016-03-14T13:38:40Zdc.date.available
Jahr der Erstellung2002dc.date.created
ZusammenfassungWe 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
Spracheendc.language.iso
Verbreitende StelleUniversität Ulmdc.publisher
LizenzStandard (Fassung vom 03.05.2003)dc.rights
Link zum Lizenztexthttps://oparu.uni-ulm.de/xmlui/license_v1dc.rights.uri
LCSHCompilers (Computer programs)dc.subject.lcsh
TitelA mechanically verified compiling specification for a realistic compilerdc.title
RessourcentypArbeitspapierdc.type
DOIhttp://dx.doi.org/10.18725/OPARU-334dc.identifier.doi
URNhttp://nbn-resolving.de/urn:nbn:de:bsz:289-vts-53499dc.identifier.urn
FakultätFakultät für Informatikuulm.affiliationGeneral
Datum der Freischaltung2005-09-05T14:49:45Zuulm.freischaltungVTS
Peer-Reviewneinuulm.peerReview
DCMI MedientypTextuulm.typeDCMI
VTS-ID5349uulm.vtsID
KategoriePublikationenuulm.category
Ulmer SchriftenreiheUlmer Informatik-Berichteuulm.seriesUlmName


Dateien zu dieser Ressource

Thumbnail

Das Dokument erscheint in:

Zur Kurzanzeige