About this paper

Appears in:
Pages: 5055-5065
Publication year: 2017
ISBN: 978-84-697-6957-7
ISSN: 2340-1095
doi: 10.21125/iceri.2017.1331

Conference name: 10th annual International Conference of Education, Research and Innovation
Dates: 16-18 November, 2017
Location: Seville, Spain

APPLYING DEDUCTIVE VERIFICATION TO BACHELOR DEGREE COURSES IN PROGRAMMING

M. Todorova1, D. Orozova2

1Sofia University (BULGARIA)
2Burgas Free University (BULGARIA)
A great number of theories, algorithms, methods and techniques of formal verification can be found in the literature. They identify three main approaches: deductive verification, equivalence checking and model checking. Chronologically, deductive verification appeared first, and it is also the most suitable for the educational purposes of introductory courses in programming. By applying it, certain system properties can be proved, such as partial and total correctness, completion of the execution, etc. To this end, the system and the property are translated into formulae of first or higher order, then a theorem prover is applied to verify the property.

This article presents its authors’ experience in applying deductive verification to the following courses: Introduction to Programming, Object-Oriented Programming and Data Structures and Programming for students of specialty Informatics and Computer Sciences in two Bulgarian universities. The usefulness of training in the field is motivated. A brief introduction of the used theories, techniques and tools is presented, as well as the process of education itself. The approaches to education are also commented: through examples, project-based and e-learning. The results are analyzed.
@InProceedings{TODOROVA2017APP,
author = {Todorova, M. and Orozova, D.},
title = {APPLYING DEDUCTIVE VERIFICATION TO BACHELOR DEGREE COURSES IN PROGRAMMING},
series = {10th annual International Conference of Education, Research and Innovation},
booktitle = {ICERI2017 Proceedings},
isbn = {978-84-697-6957-7},
issn = {2340-1095},
doi = {10.21125/iceri.2017.1331},
url = {http://dx.doi.org/10.21125/iceri.2017.1331},
publisher = {IATED},
location = {Seville, Spain},
month = {16-18 November, 2017},
year = {2017},
pages = {5055-5065}}
TY - CONF
AU - M. Todorova AU - D. Orozova
TI - APPLYING DEDUCTIVE VERIFICATION TO BACHELOR DEGREE COURSES IN PROGRAMMING
SN - 978-84-697-6957-7/2340-1095
DO - 10.21125/iceri.2017.1331
PY - 2017
Y1 - 16-18 November, 2017
CI - Seville, Spain
JO - 10th annual International Conference of Education, Research and Innovation
JA - ICERI2017 Proceedings
SP - 5055
EP - 5065
ER -
M. Todorova, D. Orozova (2017) APPLYING DEDUCTIVE VERIFICATION TO BACHELOR DEGREE COURSES IN PROGRAMMING, ICERI2017 Proceedings, pp. 5055-5065.
User:
Pass: