Change search
ReferencesLink to record
Permanent link

Direct link
Extracting analyzable models from multi-threaded programs
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
2015 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

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.

Place, publisher, year, edition, pages
2015. , 36 p.
National Category
Computer Science
URN: urn:nbn:se:liu:diva-114195ISRN: LIU-IDA/LITH-EX-A--14/066--SEOAI: diva2:788002
Subject / course
Computer and information science at the Institute of Technology
Available from: 2015-02-17 Created: 2015-02-12 Last updated: 2015-02-17Bibliographically approved

Open Access in DiVA

fulltext(260 kB)67 downloads
File information
File name FULLTEXT01.pdfFile size 260 kBChecksum SHA-512
Type fulltextMimetype application/pdf

By organisation
Department of Computer and Information ScienceThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 67 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 544 hits
ReferencesLink to record
Permanent link

Direct link