1 Search Results for "Gückel, Dominique"


Document
Automatic Derivation of Abstract Semantics From Instruction Set Descriptions

Authors: Dominique Gückel and Stefan Kowalewski

Published in: OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012)


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.

Cite as

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)


Copy BibTex To Clipboard

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

  • Refine by Classification

  • Refine by Keyword
  • 1 Hardware Description Languages
  • 1 Model Checking
  • 1 Static Analysis

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2012

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail