Formalizing the SAFECode type system

DOI10.1007/978-3-319-03545-1_14MaRDI QIDQ2938049zbMATH OpenOpenAlexFDO

Authors

Publication date 13 January 2015

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-03545-1_14

zbMATH Keywords

verificationmemory safetyLLVMSAFECode

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1949628
• Foundational certified code in the Twelf metalogical framework
• A type system for expressive security policies
• Towards proving type safety of .NET CIL
• scientific article; zbMATH DE number 2110618

Cited in

(8)

• Closed types for a safe imperative MetaML
• On the use of metatypes for safe embedded operating system extension
• A typed encoding of boxed into safe ambients
• SAFECode
• scientific article; zbMATH DE number 1949628 (Why is no real title available?)
• scientific article; zbMATH DE number 2087533 (Why is no real title available?)
• A type system for certified binaries
• Towards proving type safety of .NET CIL

Describes a project that uses

Uses Software

• CCured
• LLVM
• Coq

This page was built for publication: Formalizing the SAFECode type system

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