Highly Automated Formal Proofs over Memory Usage of Assembly Code

DOI10.1007/978-3-030-45237-7_6zbMath1483.68211OpenAlexW3017122865MaRDI QIDQ5164171

Joshua A. Bockenek, Binoy Ravindran, Freek Verbeek

Publication date: 10 November 2021

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-45237-7_6

zbMATH Keywords

formal verificationassemblymemory usagex86-64

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• CVC Lite

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Eisbach: a proof method language for Isabelle
• Isabelle/HOL. A proof assistant for higher-order logic
• Bridging the Gap: Automatic Verified Abstraction of C
• The Essence of Higher-Order Concurrent Separation Logic
• A Brief Overview of HOL4
• Communicating sequential processes
• Automated proofs of object code for a widely used microprocessor
• Compositional shape analysis by means of bi-abduction
• Computer Aided Verification
• Verification Condition Generation Via Theorem Proving
• CakeML
• A Decision Procedure for Bit-Vectors and Arrays
• An axiomatic basis for computer programming
• A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
• Hoare Logic for Realistically Modelled Machine Code
• Classes of Recursively Enumerable Sets and Their Decision Problems

This page was built for publication: Highly Automated Formal Proofs over Memory Usage of Assembly Code