Scalable certification for typed assembly language

DOI10.1007/3-540-45332-6_5MaRDI QIDQ4532093zbMATH OpenFDO

Authors Greg Morrisett, Daniel A. Grossman

Publication date 28 May 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2071/20710117

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Computing methodologies and applications (68U99)

Recommendations

• Certifying compilation and run-time code generation
• Verification, Model Checking, and Abstract Interpretation
• Investigating type-certifying compilation with Isabelle
• Programming Languages and Systems
• Verified bytecode verification and type-certifying compilation

Cited in

(8)

• Certifying compilation and run-time code generation
• Stack-based typed assembly language
• An expressive, scalable type theory for certified code
• More Typed Assembly Languages for Confidentiality
• Certifying assembly programs with trails
• scientific article; zbMATH DE number 2165694 (Why is no real title available?)
• A type system for certified binaries
• Verification, Model Checking, and Abstract Interpretation

Describes a project that uses

Uses Software

• OCaml
• TALx86

This page was built for publication: Scalable certification for typed assembly language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4532093)