By: Thang Bui

Email: This e-mail address is being protected from spambots. You need JavaScript enabled to view it

Organization: Ho Chi Minh City University of Technology

Title: Lecturer, Faculty of Computer Science & Engineering

Abstract:

Testing is the primary and common way to check the correctness of software. Testing also incurs a substantial cost in software development. Although applied widely within the industry, this method is not theoretically complete because it is impossible to have all the test cases to ensure the absence of possible flaws in software programs. In addition, it is not ideal to run a piece of potentially erroneous code on a functional system in operation. One way to tackle this is by constructing a simulated environment but this may be costly and difficult to exactly replicate the operating environment. Recently, using logic-based methods to verify software before deploying or even testing have been emerging as potential approaches to overcome these problems, at least partially. The logic-based methods, also known as formal methods in academic communities, are capable of verifying the program’s correctness without executing the actual code. In the field of software verification, there are two popular approaches: theorem proving and model checking.

In this paper, we will present the principle of software verification using theorem proving and model checking. Theorem proving can confirm the absence of bugs while model checking is strong at finding bugs and generating counterexamples. Since these two techniques suffer from theoretically high complexity when dealing with real programs, some approximation techniques are also used to make the verification process more effective. We will illustrate the practical usage of program verification via a Web-based system which is currently being developed at our faculty for checking student programming exercises.