Low Level Verification

Low Level Verification (LLV) is a user-driven software verification system focused on proving properties of C-style computer programs. The system is introduced in multiple parts, starting with a through description of the syntax and operational semantics of LLV code. The LLV execution language is presented as a simplified version of C/C++, in which data types and object constructs have been removed. The machine level implementation of LLV is not specified within the scope of this paper. Instead, the conceptual operation of the execution environment is described in a way that is easy for the reader to understand. Using this core language as a base, LLV defines propositional logic, and proof rules as tools for verification. The user may write theorems to describe the behavior of any given section of code. In LLV, a theorem specifies a conclusion in the form of propositional logic, and can be verified by a user-created proof. The LLV proof language includes all the rules available for formulating and constructing such proofs. In addition, cases requiring inductive reasoning (such as a recursive function) can be handled by a single unified approach through use of the induction proof rule. The LLV system also provides the user with other important features, such as an automatic arithmetic equation solver to handle trivial inferences. Using this as well as other tactics, LLV is presented as a method for reasoning about low level code in an efficient manner