Modular verification of SPARCv8 code

DOI10.1007/978-3-030-02768-1_14MaRDI QIDQ6166149zbMATH OpenOpenAlexFDO

Authors

Publication date 2 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Verifying branch-free assembly code in Why3
• Verification of safety properties for concurrent assembly code
• Modular verification of concurrent assembly code with dynamic thread creation and termination
• Hoare Logic for Realistically Modelled Machine Code
• Formalizing SPARCv8 instruction set architecture in Coq

Cited in

(6)

• Highly automated formal proofs over memory usage of assembly code
• Formalizing SPARCv8 instruction set architecture in Coq
• Verifying branch-free assembly code in Why3
• Hoare-style logic for unstructured programs
• Verification of safety properties for concurrent assembly code
• Using XCAP to Certify Realistic Systems Code: Machine Context Management

This page was built for publication: Modular verification of SPARCv8 code

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