License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.SSV.2011.71
URN: urn:nbn:de:0030-drops-35919
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3591/
Go to the corresponding OASIcs Volume Portal

Gückel, Dominique ; Kowalewski, Stefan

Automatic Derivation of Abstract Semantics From Instruction Set Descriptions

pdf-format:
7.pdf (0.4 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{gckel_et_al:OASIcs:2012:3591,
  author =	{Dominique G{\"u}ckel and Stefan Kowalewski},
  title =	{{Automatic Derivation of Abstract Semantics From Instruction Set Descriptions}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{71--83},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{J{\"o}rg Brauer and Marco Roveri and Hendrik Tews},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3591},
  URN =		{urn:nbn:de:0030-drops-35919},
  doi =		{10.4230/OASIcs.SSV.2011.71},
  annote =	{Keywords: Model Checking, Static Analysis, Hardware Description Languages}
}

Keywords: Model Checking, Static Analysis, Hardware Description Languages
Collection: 6th International Workshop on Systems Software Verification
Issue Date: 2012
Date of publication: 13.07.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI