---
abstract: 'MIDAS (Microprocessor Instruction and Data Abstraction System) is a specification of an Instruction Set Architecture (ISA) capable of executing binary images compiled from the C language. It was developed to demonstrate a methodology for formal construction of various ISAs in Event-B via a generic model. It is intended to be representative of typical microprocessor ISAs, but using a minimal number of defined instructions, in order to make complete refinement practical. The intention is to simplify the number and complexity of the defined instructions at the cost of compiler complexity, run-time performance and code density, without compromising representativeness. There are two variants: a stack-based machine and a randomly accessible register array machine. The two variants employ the same instruction codes, the differences being limited to register file behavior.'
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: stephen.wright@bris.ac.uk
copyright_holders: []
corp_creators: []
creators_id:
  - stephen.wright@bris.ac.uk
creators_name:
  - family: Wright
    given: Stephen
    honourific: ''
    lineage: ''
data_type: ~
date: 2009-06-04
date_type: ~
datestamp: 2009-06-06 10:51:41
department: ~
dir: disk0/00/00/00/84
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 84
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_zip.png;/84/1/MidasBundle.rar|/style/images/fileicons/application_pdf.png;/84/2/Midas_Deploy.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: unpub
issn: ~
item_issues_comment: []
item_issues_count: 0
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: Event-B Virtual Machine Instruction Set Architecture
lastmod: 2010-04-19 15:05:53
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: Deploy
refereed: ~
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 38
series: ~
skill_areas: []
source: ~
status_changed: 2009-06-06 10:51:41
subjects:
  - examples
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: 'MIDAS: A Formally Constructed Virtual Machine'
type: deploy_interest_group_item
userid: 100
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>