Integrated program verification tools in education

Automated software verification is an active field of research, which has made enormous progress both in theoretical and practical aspects. Even if not ready for large-scale industrial adoption, the technology behind automated program verifiers is now mature enough to gracefully handle the kind of p...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	De Caso, G., Garbervetsky, D., Gorín, D.
Formato:	JOUR
Materias:	automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers
Acceso en línea:	http://hdl.handle.net/20.500.12110/paper_00380644_v43_n4_p403_DeCaso
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	todo:paper_00380644_v43_n4_p403_DeCaso
record_format	dspace
spelling	todo:paper_00380644_v43_n4_p403_DeCaso2023-10-03T14:48:16Z Integrated program verification tools in education De Caso, G. Garbervetsky, D. Gorín, D. automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers Automated software verification is an active field of research, which has made enormous progress both in theoretical and practical aspects. Even if not ready for large-scale industrial adoption, the technology behind automated program verifiers is now mature enough to gracefully handle the kind of programs that arise in introductory programming courses. This opens exciting new opportunities in teaching the basics of reasoning about program correctness to novice students. However, for these tools to be effective, command-line-style user-interfaces need to be replaced. In this paper, we report on our experience using the verifying compiler for PEST in an introductory programming course as well as in a more advanced course on program analysis. PEST is an extremely basic programming language, but with expressive annotations capabilities and semantics amenable to verification. In particular, we comment on the crucial role played by the integration of this verifying compiler with the Eclipse integrated development environment. Copyright © 2012 John Wiley & Sons, Ltd. Copyright © 2012 John Wiley & Sons, Ltd. Fil:De Caso, G. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Garbervetsky, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Gorín, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. JOUR info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_00380644_v43_n4_p403_DeCaso
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers
spellingShingle	automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers De Caso, G. Garbervetsky, D. Gorín, D. Integrated program verification tools in education
topic_facet	automated program verification Eclipse plug-in education formal methods Automated program verification Eclipse Integrated Development Environment Industrial adoption Introductory programming course Plug-ins Reasoning about programs Software verification Verifying compilers Automation Education Formal methods Semantics Verification Web services Program compilers
description	Automated software verification is an active field of research, which has made enormous progress both in theoretical and practical aspects. Even if not ready for large-scale industrial adoption, the technology behind automated program verifiers is now mature enough to gracefully handle the kind of programs that arise in introductory programming courses. This opens exciting new opportunities in teaching the basics of reasoning about program correctness to novice students. However, for these tools to be effective, command-line-style user-interfaces need to be replaced. In this paper, we report on our experience using the verifying compiler for PEST in an introductory programming course as well as in a more advanced course on program analysis. PEST is an extremely basic programming language, but with expressive annotations capabilities and semantics amenable to verification. In particular, we comment on the crucial role played by the integration of this verifying compiler with the Eclipse integrated development environment. Copyright © 2012 John Wiley & Sons, Ltd. Copyright © 2012 John Wiley & Sons, Ltd.
format	JOUR
author	De Caso, G. Garbervetsky, D. Gorín, D.
author_facet	De Caso, G. Garbervetsky, D. Gorín, D.
author_sort	De Caso, G.
title	Integrated program verification tools in education
title_short	Integrated program verification tools in education
title_full	Integrated program verification tools in education
title_fullStr	Integrated program verification tools in education
title_full_unstemmed	Integrated program verification tools in education
title_sort	integrated program verification tools in education
url	http://hdl.handle.net/20.500.12110/paper_00380644_v43_n4_p403_DeCaso
work_keys_str_mv	AT decasog integratedprogramverificationtoolsineducation AT garbervetskyd integratedprogramverificationtoolsineducation AT gorind integratedprogramverificationtoolsineducation
_version_	1807324234388602880

Integrated program verification tools in education

Ejemplares similares