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

DOI10.1007/978-3-319-47958-3_3zbMath1483.68095OpenAlexW2529049110MaRDI QIDQ3179279

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

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)

Related Items (1)

AUSPICE-R

Uses Software

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

Cites Work

• Verified Software Toolchain
• Dafny: An Automatic Program Verifier for Functional Correctness
• Hoare Logic for ARM Machine Code
• A Brief Overview of HOL4
• Hoare Logic for Realistically Modelled Machine Code

This page was built for publication: AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code