Verification of programs written in assembly language using automated theorem provers

This project aims to verify programs written in assembly language through the utilization of automated theorem provers.

An assembly language ISA is a low-level programming language that provides a human-readable representation of machine code instruction. Automatic theorem provers allow the use of formal logic to model mathematical statements, algorithms, or software and to automatically verify their correctness. Given that assembly language programs are often critical for the operation of systems and devices, even minor errors in their design or implementation can have significant, potentially catastrophic consequences.

The overarching objective of this project is to first formally define and model the Instruction Set Architecture (ISA) and microcontroller behavior. Subsequently properties concerning concrete programs are proven. This to ensure program correctness and the absence of certain groups of programming errors.