Construction of a semantic model for a typed assembly language

Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations

Abstract

TypedAssembly Languages (TALs) can be used to validate the safety of assembly-language programs. However, typing rules are usually trusted as axioms. In this paper, we show how to build semantic models for typing judgments in TALs based on an induction technique, so that both the type-safety theorem and the typing rules can be proved as lemmas in a simple logic. We demonstrate this technique by giving a complete model to a sampleTAL. This model allows a typing derivation to be interpreted as a machine-checkable safety proof at the machine level.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings
EditorsBernhard Steffen, Giorgio Levi
PublisherSpringer Verlag
Pages30-43
Number of pages14
ISBN (Print)9783540208037
DOIs
StatePublished - Jan 1 2004
Event5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004 - Venice, Italy
Duration: Jan 11 2004Jan 13 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2937
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other5th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2004
CountryItaly
CityVenice
Period1/11/041/13/04

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Construction of a semantic model for a typed assembly language'. Together they form a unique fingerprint.

Cite this