A Survey of Automated Tools for Program Verification using Static analysis

PhD Qualifying Examination


Title: "A Survey of Automated Tools for Program Verification using Static 
analysis"

by

Mr. Pritom Rajkhowa


Abstract:

Software bugs in electronic systems may arise due to human error in 
writing computer programs. They may cause crashing of applications, cyber 
attacks, wrong medical reporting, accidents in aviation, automotive 
malfunctions, etc. The general practice for testing programs with a sample 
input to find any possibility of abnormal behavior is not satisfactory as 
it not possible to cover all the cases. Formal program verification 
enables mathematical means to verify the correctness of software to 
increase assurance of the program. Currently, available program 
verifications are either fully automatic or semiautomatic(interactive). 
Automated verification of computer programs has remained a topic of 
intense research for several years. During this period, different 
techniques and approaches were proposed and implemented by various tools 
to address diverse challenges in this field. Static analysis of program 
verification is a widely used technique. This report surveys current work 
on automated verification systems which use static analysis. An attempt 
has been made to present the short description of those tools highlighting 
their approaches when applied to practical problems. The merits and 
shortcomings of these tools have been discussed.


Date:			Monday, 14 August 2017

Time:                  	4:00pm - 6:00pm

Venue:                  Room 2610
                         Lifts 31/32

Committee Members:	Prof. Fangzhen Lin (Supervisor)
 			Prof. Cunsheng Ding (Chairperson)
 			Prof. Shing-Chi Cheung
 			Dr. Ke Yi


**** ALL are Welcome ****