Please use this identifier to cite or link to this item:
Title: Constraint-based verification of imperative programs
Author: Beyene, Tewodros Awgichew
Advisor: Barahona, Pedro
Keywords: Program verification
Model checking
Constraint programming
Defense Date: 2011
Publisher: Faculdade de Ciências e Tecnologia
Abstract: The continuous reduction in the cost of computing ever since the first days of computers has resulted in the ubiquity of computing systems today; there is no any sphere of life in the daily routine of human beings that is not directly or indirectly influenced by computer systems anymore. But this high reliance on computers has not come without a risk to the society or a challenge to computer scientists. As many computer systems of today are safety critical, it is crucial for computer scientists to make sure that computer systems, both the hardware and software components, behave correctly under all circumstances. In this study, we are interested in techniques of program verification that are aimed at ensuring the correctness of the software component. In this work, constraint programming techniques are used to device a program verification framework where constraint solvers play the role of typical verification tools. The programs considered are written in some subset of Java, and their specifications are written in some subset of Java Modeling Language(JML). In our framework, the program verification process has two principal steps: constraint generation and constraint solving. A program together with its specification is first parsed into a system of constraints. And then, the system of constraints is processed using constraint solvers so that the correctness of the original program is proved to hold, or not, based on the outcome of the constraint solving. The performance of our framework is compared with other well-known program verification tools using standard benchmarks, and our framework has performed quite well for most of the cases.
Description: work presented in the context of the European Master’s program in Computational Logic, as the partial requirement for obtaining Master of Science degree in Computational Logic
Appears in Collections:FCT: DI - Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
Beyene_2011.pdf437,76 kBAdobe PDFView/Open

FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.