Modular verification of SPARCv8 code

DOI10.1007/978-3-030-02768-1_14zbMATH Open1519.68144OpenAlexW2897181877MaRDI QIDQ6166149FDOQ6166149

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

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

Mathematics Subject Classification ID

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

Cited In (4)

• Verifying branch-free assembly code in Why3
• Verification of safety properties for concurrent assembly code
• Using XCAP to Certify Realistic Systems Code: Machine Context Management
• Highly automated formal proofs over memory usage of assembly code

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)