Extracting Behaviour from an Executable Instruction Set Model

Brian Campbell; Ian Stark

doi:10.1109/FMCAD.2016.7886658

Extracting Behaviour from an Executable Instruction Set Model

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

Presenting large formal instruction set models as executable functions makes them accessible to engineers and useful for less formal purposes such as simulation. However, it is more difficult to extract information about the behaviour of individual instructions for reasoning. We present a method which combines symbolic evaluation and symbolic execution techniques to provide a rule-based view of instruction behaviour, with particular application to automatic test generation for large MIPS-like models.

Original language	English
Title of host publication	Proceedings of the 16th Conference on Formal Methods in Computer - Aided Design (FMCAD 2016)
Place of Publication	Mountain View, CA, USA
Publisher	FMCAD Inc
Pages	33-40
Number of pages	8
ISBN (Electronic)	978-0-9835678-6-8
ISBN (Print)	978-1-5386-2692-4
DOIs	https://doi.org/10.1109/FMCAD.2016.7886658
Publication status	Published - 27 Mar 2017
Event	16th Conference on Formal Methods in Computer - Aided Design - Mountain View, United States Duration: 3 Oct 2016 → 6 Oct 2016 http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/

Conference

Conference	16th Conference on Formal Methods in Computer - Aided Design
Abbreviated title	FMCAD 2016
Country/Territory	United States
City	Mountain View
Period	3/10/16 → 6/10/16
Internet address	http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/

Access to Document

10.1109/FMCAD.2016.7886658

fmcad16-proc-submissionAccepted author manuscript, 260 KB

REMS: Rigorous Engineering for Mainstream Systems
Stark, I.
Other
1/03/13 → 29/02/20
Project: Research

Ian Stark
- Ian.Starked.acuk
- School of Informatics - Senior Lecturer
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active

Cite this

@inproceedings{9f5bd880cf9d4125b6d2590a2a386414,

title = "Extracting Behaviour from an Executable Instruction Set Model",

abstract = "Presenting large formal instruction set models as executable functions makes them accessible to engineers and useful for less formal purposes such as simulation. However, it is more difficult to extract information about the behaviour of individual instructions for reasoning. We present a method which combines symbolic evaluation and symbolic execution techniques to provide a rule-based view of instruction behaviour, with particular application to automatic test generation for large MIPS-like models.",

author = "Brian Campbell and Ian Stark",

year = "2017",

month = mar,

day = "27",

doi = "10.1109/FMCAD.2016.7886658",

language = "English",

isbn = "978-1-5386-2692-4",

pages = "33--40",

booktitle = "Proceedings of the 16th Conference on Formal Methods in Computer - Aided Design (FMCAD 2016)",

publisher = "FMCAD Inc",

note = "16th Conference on Formal Methods in Computer - Aided Design , FMCAD 2016 ; Conference date: 03-10-2016 Through 06-10-2016",

url = "http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/",

}

Campbell, B & Stark, I 2017, Extracting Behaviour from an Executable Instruction Set Model. in Proceedings of the 16th Conference on Formal Methods in Computer - Aided Design (FMCAD 2016). FMCAD Inc, Mountain View, CA, USA, pp. 33-40, 16th Conference on Formal Methods in Computer - Aided Design , Mountain View, California, United States, 3/10/16. https://doi.org/10.1109/FMCAD.2016.7886658

TY - GEN

T1 - Extracting Behaviour from an Executable Instruction Set Model

AU - Campbell, Brian

AU - Stark, Ian

PY - 2017/3/27

Y1 - 2017/3/27

N2 - Presenting large formal instruction set models as executable functions makes them accessible to engineers and useful for less formal purposes such as simulation. However, it is more difficult to extract information about the behaviour of individual instructions for reasoning. We present a method which combines symbolic evaluation and symbolic execution techniques to provide a rule-based view of instruction behaviour, with particular application to automatic test generation for large MIPS-like models.

AB - Presenting large formal instruction set models as executable functions makes them accessible to engineers and useful for less formal purposes such as simulation. However, it is more difficult to extract information about the behaviour of individual instructions for reasoning. We present a method which combines symbolic evaluation and symbolic execution techniques to provide a rule-based view of instruction behaviour, with particular application to automatic test generation for large MIPS-like models.

U2 - 10.1109/FMCAD.2016.7886658

DO - 10.1109/FMCAD.2016.7886658

M3 - Conference contribution

SN - 978-1-5386-2692-4

SP - 33

EP - 40

BT - Proceedings of the 16th Conference on Formal Methods in Computer - Aided Design (FMCAD 2016)

PB - FMCAD Inc

CY - Mountain View, CA, USA

T2 - 16th Conference on Formal Methods in Computer - Aided Design

Y2 - 3 October 2016 through 6 October 2016

ER -

Extracting Behaviour from an Executable Instruction Set Model

Abstract / Description of output

Conference

Access to Document

Fingerprint

Projects

REMS: Rigorous Engineering for Mainstream Systems

Profiles

Ian Stark

Cite this