Technische Universität Braunschweig
  • Studium & Lehre
    • Vor dem Studium
      • Informationen für Studieninteressierte
      • Studiengänge von A-Z
      • Bewerbung
      • Fit4TU - Self-Assessment
      • Beratungsangebote für Studieninteressierte
      • Warum Braunschweig?
    • Im Studium
      • Erstsemester-Hub
      • Semestertermine
      • Lehrveranstaltungen
      • Studien-ABC
      • Studienorganisation
      • Beratungsnavi
      • Zusatzqualifikationen
      • Finanzierung und Kosten
      • Besondere Studienbedingungen
      • Gesundheit & Wohlbefinden
      • Campusleben
    • Nach dem Studium
      • Exmatrikulation und Vorlegalisation
      • Nach dem Abschluss
      • Alumni*ae
    • Strategien und Qualitätsmanagement
      • Strategiepapiere für Studium und Lehre
      • Studienqualitätsmittel
      • Studiengangsentwicklung
      • Qualitätsmanagement
      • Systemakkreditierung
      • Rechtliche Grundlagen
      • TU Lehrpreis
    • Für Lehrende
      • Informationen für Lehrende
      • Konzepte
      • Lernmanagementsystem Stud.IP
    • Kontakt
      • Studienservice-Center
      • Sag's uns - in Studium und Lehre
      • Zentrale Studienberatung
      • Immatrikulationsamt
      • Abteilung 16 - Studium und Lehre
      • Career Service
      • Projekthaus
  • Forschung
    • Forschungsprofil
      • Forschungsschwerpunkte
      • Exzellenzcluster der TU Braunschweig
      • Forschungsprojekte
      • Forschungszentren
      • Forschungsprofile der Professuren
    • Frühe Karrierephase
      • Förderung in den frühen Phasen der wissenschaftlichen Karriere
      • Promotion
      • Postdocs
      • Nachwuchsgruppenleitung
      • Junior Professur und Tenure-Track
      • Habilitation
      • Service-Angebote für Wissenschaftler*innen
    • Forschungsdaten & Transparenz
      • Transparenz in der Forschung
      • Forschungsdaten
      • Open Access Strategie
      • Digitale Forschungsanzeige
    • Forschungsförderung
      • Netzwerk Forschungsförderung
      • Datenbanken und Stiftungen
    • Kontakt
      • Forschungsservice
      • Graduiertenakademie
  • International
    • Internationale Studierende
      • Warum Braunschweig?
      • Studium mit Abschluss
      • Austauschstudium
      • TU Braunschweig Summer School
      • Geflüchtete
      • International Student Support
    • Wege ins Ausland
      • Studium im Ausland
      • Praktikum im Ausland
      • Lehren und Forschen im Ausland
      • Arbeiten im Ausland
    • Internationale Forschende
      • Welcome Support
      • Promotionsstudium
      • Service für gastgebende Einrichtungen
    • Sprachen und interkulturelle Kompetenzvermittlung
      • Deutsch lernen
      • Fremdsprachen lernen
      • Interkulturelle Kompetenzvermittlung
    • Internationales Profil
      • Internationalisierung
      • Internationale Kooperationen
      • Strategische Partnerschaften
      • Internationale Netzwerke
    • International House
      • Wir über uns
      • Kontakt & Sprechstunden
      • Aktuelles und Termine
      • International Days
      • 5. Studentische Konferenz: Internationalisierung der Hochschulen
      • Newsletter, Podcast & Videos
      • Stellenausschreibungen
  • Die TU Braunschweig
    • Unser Profil
      • Ziele & Werte
      • Ordnungen und Leitlinien
      • Allianzen & Partner
      • Hochschulentwicklung 2030
      • Stiftungsuniversität
      • Internationale Strategie
      • Fakten & Zahlen
      • Unsere Geschichte
    • Karriere
      • Arbeiten an der TU
      • Stellenmarkt
      • Berufsausbildung an der TU
    • Wirtschaft & Unternehmen
      • Unternehmensgründung
      • Freunde & Förderer
    • Öffentlichkeit
      • Veranstaltungskalender
      • Check-in für Schüler*innen
      • Hochschulinformationstag (HIT)
      • Kinder-Uni
      • Das Studierendenhaus
      • Gasthörer*innen & Senior*innenstudium
      • Nutzung der Universitätsbibliothek
    • Presse & Kommunikation
      • Stabsstelle Presse und Kommunikation
      • Medienservice
      • Ansprechpartner*innen
      • Tipps für Wissenschaftler*innen
      • Themen und Stories
    • Kontakt
      • Allgemeiner Kontakt
      • Anreise
      • Für Hinweisgeber
  • Struktur
    • Leitung & Verwaltung
      • Das Präsidium
      • Stabsstellen
      • Verwaltung
      • Organe, Statusgruppen und Kommissionen
    • Fakultäten
      • Carl-Friedrich-Gauß-Fakultät
      • Fakultät für Lebenswissenschaften
      • Fakultät Architektur, Bauingenieurwesen und Umweltwissenschaften
      • Fakultät für Maschinenbau
      • Fakultät für Elektrotechnik, Informationstechnik, Physik
      • Fakultät für Geistes- und Erziehungswissenschaften
    • Institute
      • Institute von A-Z
    • Einrichtungen
      • Universitätsbibliothek
      • Gauß-IT-Zentrum
      • Zentrale Personalentwicklung
      • International House
      • Projekthaus
      • Transferservice
      • Hochschulsportzentrum
      • Einrichtungen von A-Z
    • Studierendenschaft
      • Studierendenparlament
      • Fachschaften
      • Studentische Wahlen
    • Lehrer*innenbildung
      • Lehrer*innenfortbildung
      • Forschung
    • Chancengleichheit
      • Gleichstellung
      • Familie
      • Diversität
    • Kontakt
      • Personensuche
  • Suche
  • Schnellzugriff
    • Personensuche
    • Webmail
    • cloud.TU Braunschweig
    • Messenger
    • Mensa
    • TUconnect (Studierendenportal)
    • Lehrveranstaltungen
    • Im Notfall
    • Stud.IP
    • UB Katalog
    • Status GITZ-Dienste
    • Störungsmeldung GB3
    • IT Dienste
    • Informationsportal (Beschäftigte)
    • Beratungsnavi
    • Linksammlung
    • DE
    • EN
    • IBR YouTube
    • Facebook
    • Instagram
    • YouTube
    • LinkedIn
    • Mastodon
Menü
  • Struktur
  • Fakultäten
  • Carl-Friedrich-Gauß-Fakultät
  • Institute
  • Institut für Betriebssysteme und Rechnerverbund
Logo IBR
IBR Login
  • Institut für Betriebssysteme und Rechnerverbund
    • News
    • Wir über uns
      • Gesamtes Team
      • Anreise
      • Raumplan
      • Projekte
      • Veröffentlichungen
      • Software
      • News Archiv
    • Connected and Mobile Systems
      • Team
      • Lehrveranstaltungen
      • Abschlussarbeiten
      • Projekte
      • Veröffentlichungen
      • Software
      • Datensätze
    • Verlässliche Systemsoftware
      • Übersicht
      • Team
      • Lehre
      • Arbeiten & Jobs
      • Forschung
      • Publikationen
    • Algorithmik
      • Team
      • Lehrveranstaltungen
      • Abschlussarbeiten
      • Projekte
      • Veröffentlichungen
    • Mikroprozessorlabor
    • Studium
      • Sommersemester 2025
      • Wintersemester 2024/2025
      • Abschlussarbeiten
    • Service
      • Bibliothek
      • Mailinglisten
      • Webmail
      • Knowledgebase
      • Wiki
      • Account Management
      • Service-Status
    • Spin-Offs
      • Docoloc
      • bliq (formerly AIPARK)
      • Confidential Technologies
    • Forschungsverbünde
      • IST.hub

Formal modeling of the 64-bit RISC-V instruction set architecture

BetreuerDr. Sören Tempel
IBR GruppeVSS (Prof. Dietrich)
ArtBachelorarbeit
Statusoffen

Context

RISC-V is a modern open standard instruction set architecture (ISA). The ISA is the central interface between the hardware and the software and specifies the instructions supported by a given processor. Commonly, the semantics of these instructions—and edge cases in this regard—are described in natural language. The natural language definition of the RISC-V ISA can be found here.

Problem

Considering that natural language is ambiguous, an implementation of these specified instructions semantics (e.g., for a RISC-V simulator) is a manual process, requiring a transformation of the natural language specification to executable code. Naturally, considering the complexity of the specification, errors can occur during this manual transformation.

In order to prevent such errors, prior work has proposed the use of a formal machine-readable language to describe ISA instruction semantics. These formal languages are unambiguous and thus machine-readable. They are beneficial for various use-case, such as code generation, testing, documentation, or binary analysis. Recognizing the potential of these formal languages, RISC-V provides an official formal specification in the SAIL language.

However, SAIL is a non-executable formal specification requiring the implementation of a compiler to transform it to executable code. For many execution-based tasks (e.g., simulation or binary analysis), this creates a lot of duplicate work. Therefore, executable formal specifications have received increased attention in recent years.

In prior work, we have developed a versatile executable formal model of the RISC-V architecture and have implemented several interpreters for this specification, most recently a symbolic interpreter. Presently, the formal specification only covers 32-bit RISC-V, however as a basis for future work, we would like to extend our symbolic interpreter to 64-bit RISC-V. To this end, our formal executable specification should be extended in this thesis to support 64-bit RISC-V (RV64). This should be achieved by making the specification parameterisable over the word size, thereby requiring only minor changes in the description of instruction semantics. Naturally, correctness aspects of the extended specification should also be examined to some degree in the thesis.

Requirements

  • Solid understanding of computer architecture
  • Proficiency in functional programming, ideally prior experience with Haskell (or a similar language)
  • Analytical skills to evaluate correctness aspects of the formalized RV64 specification

More Information

For more information, you can refer to the following resources

  • The Hackage package for our formal RISC-V specification (includes API documentation)
  • The source code of our executable formal specification
  • The formal description of the RISC-V base instruction set

Further, the following papers might be useful as a starting point:

  • Versatile and Flexible Modelling of the RISC-V Instruction Set Architecture
  • Accurate and Extensible Symbolic Execution of Binary Code based on Formal ISA Semantics
  • ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS

Recommended reading to get started with Haskell: Learn You a Haskell.


aktualisiert am 12.08.2025, 16:02 von System Account vss-deploy

Für alle

Stellen der TU Braunschweig
Jobbörse des Career Service
Merchandising
Sponsoring- & Spendenleistungen
Drittmittelgeförderte Forschungsprojekte
Vertrauenspersonen für Hinweisgeber

Für Studierende

Semestertermine
Lehrveranstaltungen
Studiengänge von A-Z
Informationen für Erstsemester
TUCard

Interne Tools

Status GITZ-Dienste
Handbuch für TYPO3 (Intern)
Corporate Design-Toolbox (Intern)
Glossar (DE-EN)
Meine Daten ändern
Hochschulöffentliche Bekanntmachungen

Kontakt

Technische Universität Braunschweig
Universitätsplatz 2
38106 Braunschweig
Postfach: 38092 Braunschweig
Telefon: +49 (0) 531 391-0

Anreise

© Technische Universität Braunschweig
Impressum Datenschutz Barrierefreiheit