Automatic Derivation of Abstract Semantics From Instruction Set Descriptions

Authors Dominique Gückel, Stefan Kowalewski

Thumbnail PDF


  • Filesize: 378 kB
  • 13 pages

Document Identifiers

Author Details

Dominique Gückel
Stefan Kowalewski

Cite AsGet BibTex

Dominique Gückel and Stefan Kowalewski. Automatic Derivation of Abstract Semantics From Instruction Set Descriptions. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 71-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Abstracted semantics of instructions of processor-based architectures are an invaluable asset for several formal verification techniques, such as software model checking and static analysis. In the field of model checking, abstract versions of instructions can help counter the state explosion problem, for instance by replacing explicit values by symbolic representations of sets of values. Similar to this, static analyses often operate on an abstract domain in order to reduce complexity, guarantee termination, or both. Hence, for a given microcontroller, the task at hand is to find such abstractions. Due to the large number of available microcontrollers, some of which are even created for specific applications, it is impracticable to rely on human developers to perform this step. Therefore, we propose a technique that starts from imperative descriptions of instructions, which allows to automate most of the process.
  • Model Checking
  • Static Analysis
  • Hardware Description Languages


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads