Utilize este identificador para referenciar este registo: http://hdl.handle.net/10362/7965
Título: Constraint-based verification of imperative programs
Autor: Beyene, Tewodros Awgichew
Orientador: Barahona, Pedro
Palavras-chave: Program verification
Model checking
Constraint programming
Data de Defesa: 2011
Editora: Faculdade de Ciências e Tecnologia
Resumo: 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.
Descrição: 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
URI: http://hdl.handle.net/10362/7965
Aparece nas colecções:FCT: DI - Dissertações de Mestrado

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
Beyene_2011.pdf437,76 kBAdobe PDFVer/Abrir

FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.