AUSPICE-R: automatic safety-property proofs for realistic features in machine code

DOI10.1007/978-3-319-47958-3_3MaRDI QIDQ3179279zbMATH OpenOpenAlexFDO

Authors Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi, P. Narasimhan

Publication date 21 December 2016

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

Full work available at URL https://doi.org/10.1007/978-3-319-47958-3_3

Mathematics Subject Classification ID

Theory of software (68N99)

Recommendations

• Automatic construction of Hoare proofs from abstract interpretation results.
• Highly automated formal proofs over memory usage of assembly code
• Machine assisted proof of ARMv7 instruction level isolation properties
• Algebraic Methodology and Software Technology
• scientific article; zbMATH DE number 1903378

Cites work

• A Brief Overview of HOL4
• Dafny: an automatic program verifier for functional correctness
• Hoare Logic for ARM Machine Code
• Hoare Logic for Realistically Modelled Machine Code
• Verified software toolchain (invited talk)

Cited in

(3)

• Machine assisted proof of ARMv7 instruction level isolation properties
• AUSPICE-R
• Algebraic Methodology and Software Technology

Describes a project that uses

Uses Software

• Dafny
• MiBench
• HOL
• Toolchain
• seL4
• SeaHorn
• ARMor
• Verasco

This page was built for publication: AUSPICE-R: automatic safety-property proofs for realistic features in machine code

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