Formalizing SPARCv8 instruction set architecture in Coq

DOI10.1007/978-3-319-69483-2_18MaRDI QIDQ5045393zbMATH OpenOpenAlexFDO

Authors

Publication date 4 November 2022

Published in Dependable Software Engineering. Theories, Tools, and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-69483-2_18

zbMATH Keywords

Coqoperational semanticsSPARcv8verification

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Theory of operating systems (68N25) Semantics in the theory of computing (68Q55) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• A trustworthy monadic formalization of the ARMv7 instruction set architecture
• scientific article; zbMATH DE number 1670745
• Modular verification of SPARCv8 code
• scientific article; zbMATH DE number 1670746
• Machine assisted proof of ARMv7 instruction level isolation properties

Cited in

(4)

• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• Machine assisted proof of ARMv7 instruction level isolation properties
• A trustworthy monadic formalization of the ARMv7 instruction set architecture
• Modular verification of SPARCv8 code

This page was built for publication: Formalizing SPARCv8 instruction set architecture in Coq

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