Abstract
In contemporary computational research, the formal specification and verification of assembly languages are essential in ensuring software reliability and correctness. The weakest precondition methodology is a fundamental method in formal verification, which identifies the minimal conditions under which a program’s pre-execution state meets a specified state or a post-condition after execution of the specific code block. This research focuses on the operational semantics modeling of RISC-V instructions, a foundational step in establishing a robust verification framework for assembly language programming. Leveraging the ACL2 formal method, this research defines the operational semantics for a select group of RISC-V instructions, paving the way for a systematic and rigorous approach to verifying assembly code. The ACL2 system's advanced proof automation capabilities are utilized to model these operational semantics, which are essential for understanding and predicting the behavior of low-level software. This preliminary work lays the groundwork for future developments in integrating the weakest precondition methodology with operational semantics, highlighting its critical role within the broader scope of formal verification. Our ultimate goal is to establish mathematical proofs of equivalence between operational and weakest precondition semantics for RISC-V assembly language instructions. We aim to prove the weakest preconditions for assembly language programs, ensuring their correctness and reliability. This effort marks a significant advancement in the field by addressing the challenges of assembly language verification, setting the stage for further research into comprehensive formal verification methods for low-level code.