Paper Info
Title
An Innovative Teaching Tool Based On Semantic Tableaux For Verification And Debugging Of Imperative Programs
Abstract
While Computational Logic plays an important role in several areas of Computer Science (CS), most educational software developed for teaching logic is not suitable to be used directly in large portions of the CS education domain where the application of logical notions is usually required. In this paper we describe an innovative methodology based on a logic teaching tool on semantic tableaux that has been developed to help students to use logic as a formal proof technique in other advanced topics of CS, such as the verification of algorithms, the algorithmic debugging of programs, and the derivation of algorithms from logical specifications, which are foundations of good development of software. We present the results of the evaluation of this tool by means of several educational experiences during the academic year 2009/2010. From these results we conclude that the use of the tool in current CS teaching can help our students to understand more advanced CS concepts and clarify the formal process involved in the design and analysis of correct and efficient imperative programs.
Year
DOI
Venue
2011
10.1016/j.procs.2011.04.208
PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE (ICCS)
Keywords
Field
DocType
Tools to aid in teaching, Semantic tableaux, Formal verification, Algorithmic debugging
Educational software,Computational logic,Programming language,Computer science,Academic year,Software,Formal verification,Formal proof,Debugging,Algorithmic program debugging
Journal
Volume
ISSN
Citations 
4
1877-0509
0
PageRank 
References 
Authors
0.34
2
2
Name
Order
Citations
PageRank
Rafael del Vado V́ırseda19713.26
Fernando Ṕerez Morente200.34