文章基本信息

标题：Automatic Derivation of Abstract Semantics From Instruction Set Descriptions
本地全文：下载
作者：Dominique G{\"u}ckel ; Stefan Kowalewski
期刊名称：OASIcs : OpenAccess Series in Informatics
电子版ISSN：2190-6807
出版年度：2012
卷号：24
页码：71-83
DOI：10.4230/OASIcs.SSV.2011.71
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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