Memory models for the formal verification of assembler code using bounded model checking

Wolfgang Ecker, Volkan Esen, Thomas Steininger, Martin Zambaldi

Publikation: Beitrag in Buch/Bericht/KonferenzbandKonferenzbeitragBegutachtung

3 Zitate (Scopus)

Abstract

The formal verification of assembler code using hardware verification tools requires memory components which e.g. hold the code itself and the processed data. Since the count of variables to be proven usually rises with both data-size and address-space, complexity boundaries of formal tools can be reached quickly. Since bounded model checking (BMC) always involves a certain time window and therefore the count of memory accesses is limited, it is possible to optimize the applied memory as far as the address-space and the size in the count of gates is concerned. In this paper we introduce various memory models, which decrease the complexity of formal proofs by applying such optimizations. We will provide examples of models with limitations either of the address-space or the amount of storable data. Our analysis will show that these models remarkably enhance the performance, while verifying the instruction-set of a given processor-unit with our in-house BMC-Tool.

OriginalspracheEnglisch
TitelProceedings - Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing
Redakteure/-innenJ. Gustafsson, T. Aoki, I. Lee
Seiten129-135
Seitenumfang7
DOIs
PublikationsstatusVeröffentlicht - 2004
VeranstaltungProceedings - Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing - Vienna, Österreich
Dauer: 12 Mai 200414 Mai 2004

Publikationsreihe

NameProceedings - Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing

Konferenz

KonferenzProceedings - Seventh IEEE International Symposium on Object-Oriented Real-Time Distributed Computing
Land/GebietÖsterreich
OrtVienna
Zeitraum12/05/0414/05/04

Fingerprint

Untersuchen Sie die Forschungsthemen von „Memory models for the formal verification of assembler code using bounded model checking“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren