Skip to main content

AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code

Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi, Priya Narasimhan

DOI 10.1007/978-3-319-47958-3_3 dblp BibTeX

Abstract elided by the publisher.

Related papers

Verification of safety properties for concurrent assembly code ICFP 2004
A generic annotation inference algorithm for the safety certification of automatically generated code GPCE 2006
End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers CAV 2022
RustBelt: securing the foundations of the rust programming language POPL 2018
Denali: A practical algorithm for generating optimal code TOPLAS 2006
Random testing of a higher-order blockchain language (experience report) ICFP 2022
Modular verification of concurrent assembly code with dynamic thread creation and termination ICFP 2005
Lang-n-Prove: A DSL for Language Proofs SLE 2022