Extension Of The Design And Implementation Of The Verification Condition Generator In Safe C Verifier

Software in traffic,power,military and other key domains need to be more and more reliabile and safe because it is seriously related to the safety of people and property.C language is widely used in the software development in the above domains.The flexible and efficient features of the C language allow the programmer to do fairly low-level operations,but it also causes the C program to easily contain the defects of illegal pointer deference,memory leakage,buffer overflow,and so on.Formal verification is an approach for strictly guaranteeing program reliability.Our team is developing a program verifier for the Safe C language,that performs deductive reasoning for C programs with program annotations to verify whether or not the program meets the expected specification.The function of the verification condition generator in Safe-C verifier is to support the syntax of the Safe C language and the specification language,to implement the calculus rules of each statement,to traverse the source program according to the calculus rules,and to produce the assertions and reasonable and effective verification conditions at each program point.This thesis extends the verification condition generator in the program verifier.The main work of this thesis and my contributions are listed as follows:Firstly,I have participated in the design of logic variables,ghost code,string type,named behavior protocol and multi-function protocol in the SCSL specification language,which improves the expressive ability of the specification language.I have designed and implemented the corresponding calculus rules independently.Secondly,I have designed and implemented the calculus rules of jump statements goto,continue,break,switch and function call statements based on Hoare logic,so that the verifier can support more C syntax and control structure and its scope is expanded.At the same time,I have implemented the procedures for expansion of fully quantified assertions and predicates before assignment statements,which reduces the burden of the automatic theorem prover.Thirdly,according to the semantics of C language,a stack area memory model has been proposed,which can support data types such as structures and multiple pointers.Based on this model,the operation rules such as addressing,multi-level dereference and pointer relation operations are implemented.In addition,based on this model I have proposed an algorithm to identify aliases,which can perform aliasing replacement accurately before applying Hoare assignment rules.Due to the above extentions,the verification capability the program verifier has been enhanced.Many examples of C programs have been successfully verified,including classic algorithms such as quick sort,bubble sort,string matching and so on.