A case for teaching program verification: Its importance in the CS curriculum
Author: 
Ali MiliAuthors Info & Claims
Abstract
Because of its relevance to program analysis and, ultimately, to program synthesis, the area of formal verification of program correctness is an important part of the education of the programmer and the computer scientist. A case is presented in this paper to advocate the teaching of the formal verification of computer programs. This case is based on three major arguments:
- The Why, i.e. the need for including a course on program verification in the computer science curriculum,
- The What, i.e. the technical contents of such a course as highlighted by the current state of the art,
- The How, i.e. the logistic feasibility of such a course within a fifteen-week semester.
References
[1]
Anderson R. "Proving programs correct". John Wiley and Sons. 1979.
[2]
Berg H., W. Boebert, W. Franta, T. Moher. "A Survey of formal methods of program verification and specification". Prentice Hall, 1982.
[3]
Burstall R. "Program proving as hand simulation with a little induction". Information Processing 1974. North Holland.
[4]
Chang C. and R. Lee. "Symbolic Logic and mechanical theorem proving". Academic Press. 1973.
[5]
DeBakker J. "Mathematical Theory of program correctness". Prentice Hall International. 1980.
[6]
Floyd R. "Assigning meanings to programs". Symposium on applied mathematics. Vol. 19, 1967.
[7]
Gries D., editor. "Programming methodology". Springer Verlag. 1978.
[8]
Gries D. "Is Sometime ever better than Alway". ACM TOPLAS. 1(2). 1979.
[9]
Gries, D. "The Science of programming", Springer Verlag. 1981.
[10]
Hoare A. "An axiomatic basis of computer programming". CACM, 12(10). October 1969.
[11]
Li&numl;ger R., H. Mills and B. Witt. "Structured programming". Addison Wesley. 1979.
[12]
Liu C.L. "Elements of discrete mathematics". McGraw Hill, 1977.
[13]
Manna Z. "Mathematical theory of computation". McGraw Hill, 1974.
[14]
Manna Z. "Is Sometime sometimes better than Always". CACM, 21(2). February 1978.
[15]
Manna Z. and R. Waldinger. "The logic of computer programming". IEEE-TSE. SE-4(3). May 1978.
[16]
Mendelson E. "Introduction to mathematical logic". D. Van Nostrand. 1979.
[17]
Mills H., R. Austing, V. Basili, J. Gannon, R. Hamlet, J. Kohl and B. Schneiderman. "The calculus of computer programming". Private communication. To appear by Allyn and Bacon, Newton, Ma.
[18]
Owicki S. and D. Gries. "An axiomatic proof technique for parallel programs". Acta Informatica. Vol 6. 1976.
[19]
Yeh R., editor. "Current trends in programming methodology". Vol. 2, Prentice Hall, 1977.
[20]
Yeh R., editor. "Current Trends in programming methodology". Vol. 4. Prentice Hall, 1977.
Index Terms
- A case for teaching program verification: Its importance in the CS curriculum
Recommendations
A case for teaching program verification: Its importance in the CS curriculum
SIGCSE '83: Proceedings of the fourteenth SIGCSE technical symposium on Computer science educationBecause of its relevance to program analysis and, ultimately, to program synthesis, the area of formal verification of program correctness is an important part of the education of the programmer and the computer scientist. A case is presented in this ...
Teaching formal methods for program development and verification (Panel Session)
SIGCSE '83: Proceedings of the fourteenth SIGCSE technical symposium on Computer science educationA. Joe Turner
The role of formal methods for program development and verification in computer science curricula will be discussed. The panel members will address the questions
1) What should be taught?
2) When should it be taught?
3) What are the ...
A review of an engineering teaching apprenticeship program
FIE '11: Proceedings of the 2011 Frontiers in Education ConferenceA teaching apprentice program was implemented for senior-level engineering graduate students at the University of Notre Dame during the spring of 2009. The goal of the program was to offer a mentored teaching experience to graduate students that would ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
February 1983307 pages
Copyright © 1983 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 February 1983
Published in SIGCSE Volume 15, Issue 1
Check for updates
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 354Total Downloads
- Downloads (Last 12 months)77
- Downloads (Last 6 weeks)10
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in