Back to first pageBack to first page Centre for Artificial Intelligence of UNL
Browse our site
You are here:

Publication details

Go back
Publication details
Main information
Constraint based Certification of Imperative Programs
October 2011
Beye
In this work, constraint programming techniques are used for program verification with constraint solvers playing the role typical verification tools play in typical program verification set ups. The programs considered are written in some subset of the Java programming language, and their preconditions and postconditions are written in some subset of the Java Modling Language(JML). The program verification process has two principal steps: constraint generation and constraint solving. A program together with its precondition and postcondition is first parsed into a system of constraints. 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.
M. Sc. dissertation
Tewodros A. Beyene
Pedro Barahona and
Faculdade de Ciências e Tecnologia da UNL
-
-
Export formats
Tewodros A. Beyene, Constraint based Certification of Imperative Programs, Pedro Barahona and (superv.), Faculdade de Ciências e Tecnologia da UNL, October 2011.
<b>Tewodros A. Beyene</b>, <u>Constraint based Certification of Imperative Programs</u>, Pedro Barahona and (superv.), Faculdade de Ciências e Tecnologia da UNL, October 2011.
@mastersthesis {Beye, author = {Tewodros A. Beyene}, title = {Constraint based Certification of Imperative Programs}, school = {Faculdade de Ci{\^e}ncias e Tecnologia da UNL}, note = {Pedro Barahona and (superv.); }, abstract = {In this work, constraint programming techniques are used for program verification with constraint solvers playing the role typical verification tools play in typical program verification set ups. The programs considered are written in some subset of the Java programming language, and their preconditions and postconditions are written in some subset of the Java Modling Language(JML). The program verification process has two principal steps: constraint generation and constraint solving. A program together with its precondition and postcondition is first parsed into a system of constraints. 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.}, month = {October}, year = {2011}, }
Publication's urls
/publications/view.php?code=b7980af0dc61d9dc42401adbd9a29f1e
/publications/view.php?code=Beye
Go back
Centre for Artificial Intelligence of UNL
Departamento de Informática, FCT/UNL
Quinta da Torre 2829-516 CAPARICA - Portugal
Tel. (+351) 21 294 8536 FAX (+351) 21 294 8541

Fundacao_FCT