AbstractsComputer Science

As technology evolves, the need to use software for critical applications increases. It is then required that this software will always behave correctly. Verification is the process of formally proving that a program is correct. Model checking is a technique used to perform verification, which has been successful with finite state concurrent programs. In the recent years, there has been progress in the area of the verification of infinite state concurrent programs. There can be several sources of infiniteness. Relevant to this thesis are recent model checking techniques developed at LiU, that can automatically establish correctness for programs manipulating variables that range over infinite domains, and spawning arbitrary many threads, which can synchronize using shared variables, barriers, semaphores etc. These techniques resulted in the tool PACMAN for the verification of multi-threaded programs. The aim of this thesis is to extract analyzable models from multi-threaded C programs, in order to use them for verifying the program that they describe, by using PACMAN. In addition, we augment the C programming language to allow the possibility of expressing some important concepts of multi-threaded programs, such as non-determinism, atomicity etc, with the use of the traditional C syntax. In a following step, we target PACMAN's input format, in order to verify our extracted models. Such verification engines usually accept as input the description of a multi-threaded program expressed in some modeling language. We, therefore, translate a minimum subset of the C programming language, which has been augmented, to effectively describe a multithreaded program, to PACMAN's input format and then pass the description to the engine. In the context of this thesis, we have successfully defined a set of annotation for the C programming language, in order to assist the description of multi-threaded programs. We have implemented a tool that effectively translates annotated C code into the modeling language of PACMAN. The output of the tool is later passed to the verification engine. As a result, we have contributed to the automation of verifying multi-threaded C programs.