Survey on Software Verification

PhD Qualifying Examination


Title: "Survey on Software Verification"

by

Mr. Yueqi LI


Abstract:

This report surveys some major work on software verification. In particular, we 
focus on source code and implementation verification. Implementation and source 
code level verification is important because most software is still developed 
manually by developers and most of software cannot be built via automatic code 
generation. In recent decade, people have developed verification techniques to 
perform verification directly on source code level and implementation level. 
Some major challenges of applying verification techniques on source code level 
or implementation level are explained in this survey and the approaches to 
addressing these challenges are surveyed. We classify the verification 
techniques into three big categories, which are concrete model checking, 
symbolic model checking, and abstract model checking. Concrete model checking 
techniques are mostly used to check concurrent programs. Symbolic model 
checking and abstract model checking techniques are used to address the 
scalability caused by huge or infinite input space and program states. We also 
briefly discuss the relation between dynamic analysis also called testing and 
model checking. The recent development of model checking and symbolic execution 
allows automatic code generation, which greatly reduces human effort to develop 
test cases. We also discuss how the verification techniques can be used to 
improve software quality and productivity in the future based on today’s 
development of techniques.


Date:                   Wednesday, 31 August 2011

Time:                   3:30pm - 5:30pm

Venue:                  Room 3501
                         lifts 25/26

Committee Members:	Prof. Shing-Chi Cheung (Supervisor)
                         Dr. Charles Zhang (Chairperson)
 			Dr. Lin Gu
 			Dr. Sunghun Kim


**** ALL are Welcome ****