Abstract
How can a computer program developer ensure that a program actually implements its intended purpose? This article describes a method for checking the correctness of certain types of computer programs. The method is used commercially in the development of programs implemented as integrated circuits, and is applicable to the development of “control-intensive” software programs as well. “Divide-and-conquer” techniques central to this method apply to a broad range of program verification methodologies.
This article is derived from my article entitled Program Verification, which appeared in the Notices of the American Mathematical Society, vol. 47, May 2000, and is excerpted here with their permission.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. Barwise, Mathematical proofs of computer system correctness, Notices Amer. Math. Soc. 36 (1989), 844–851.
W. W. Bledsoe and D. W. Loveland (eds.), Automated Theorem Proving: After 25 Years, Contemporary Math., vol. 9, Amer. Math. Soc., Providence, 1984; especially R. S. Boyer and J. S. Moore, Proof-checking, theorem-proving and program verification, pp. 119–132.
E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, Lecture Notes in Computer Science, vol. 131, Springer-Verlag, 1981.
E. M. Clarke Jr., O. Grumberg, and D. Peled, Model Checking, MIT Press, 1999.
R. DeMillo, R. Lipton, and A. Perlis, Social processes and proofs of theorems and programs, Comm. ACM22 (1979), 271–280.
E. W. Dijkstra, Hierarchical ordering of sequential processes, Acta Informatica 1 (1971), 115–138.
E. A. Emerson, Temporal and modal logic, Handbook of Theoretical Computer Science, vol. B, Elsevier, 1990, pp. 995–1072.
P. Halmos, Lectures on Boolean Algebras, Springer-Verlag, 1974.
R. P. Kurshan, Computer-aided Verification of Coordinating Processes—The Automata-Theoretic Approach, Princeton University Press, 1994.
K. L. McMillan, Symbolic Model Checking, Kluwer, 1993.
S. Schroeder, Turning to formal verification, Integrated System Design Magazine, Sept. 1997, 1–5.
M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program verification, Proc. (1st) IEEE Symposium on Logic in Computer Science, (1981), 322–331.
N. Wirth, Program development by stepwise refinement, Comm. ACM 14 (1971), pp. 221–227.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kurshan, R.P. (2002). Model Checking and Abstraction. In: Koenig, S., Holte, R.C. (eds) Abstraction, Reformulation, and Approximation. SARA 2002. Lecture Notes in Computer Science(), vol 2371. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45622-8_1
Download citation
DOI: https://doi.org/10.1007/3-540-45622-8_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43941-7
Online ISBN: 978-3-540-45622-3
eBook Packages: Springer Book Archive