Approximations, anomalies and "the proof of correctness wars"
Page 3
Abstract
We discuss approaches to establishing "correctness" and describe the usefulness of logic-based model checkers for producing better practical system designs. While we could develop techniques for "constructing correctness" in our theoretical behavioral-modeling research, when applied to Real World processes such as software development only approximate correctness might be established and anomalous behaviors subsequently found. This we view as a positive outcome since resultant adaptation, or flaw detection and correction, may lead to improved development and designs. We find researchers employing model checking as a formal methods tool to develop empirical techniques have reached similar conclusions. Thus we cite some applications of model checking to generate tests and detect defects in such Real World processes as aviation system development, fault-detection systems, and security.
References
[1]
ACM Forum on "Resolving the Program-Verification Debate", responses to Glass {11} by C. W. Neville and by J. H. Fetzer, Communications of the ACM, Vol. 45, No. 12, December 2002, pp. 11--13.
[2]
Alexander, P. and C. Kong, "Rosetta: Semantic Support for Model-Centered Systems-Level Design", IEEE Computer, Vol. 34, No. 11, November 2001, pp. 64--70.
[3]
Lectures presented at the Association for Symbolic Logic 2002 Annual Meeting, University of Nevada Las Vegas, June 2002. Lectures: Clarke, E. M., Jr., "Symbolic Model Checking 'with' and 'without' BDDs", Emerson, E. A., "Parameterized Model Checking"; Fass, L. F., "Modeling 'as Best One Can'"; Jha, S. "Applications of Model Checking to Security"; Shankar, N. "Little Engines of Proof"; Sistla, A. P., "Symmetry and Model Checking"; Vieth, H., "Counterexamples in Model Checking". abstracted in Meeting Booklet, and in The Bulletin of Symbolic Logic, Vol. 9, No. 1 (March 2003), pp. 51--70.
[4]
Eischen, K., "Software Development: An Outsider's View", IEEE Computer, Vol. 35, No. 5, May 2002, pp. 36--44.
[5]
Fass, L. F., "A Common Basis for Inductive Inference and Testing", in Proceedings. of the 7th Pacific Northwest Software Quality Conference., Portland, OR, September 1989, pp. 183--200.
[6]
Fass, L. F., "Electronic Commerce is an Intriguing Domain for AI Learning Theory", in Papers from the AAAI Workshop on Artificial Intelligence for Electronic Commerce, T. Finn and B. Grosof (Editors), Orlando FL, July 1999, AAAI Press, WS99--01, pp. 115--116.
[7]
Fass, L. F., "Determining Software Models that Are Less Incorrect", in {12}, pp. 113--116.
[8]
Fetzer, J. H. "Program Verification: the Very Idea", Communications of the ACM, Vol. 31, No. 9, September 1988, pp. 1048--1063.
[9]
Fischer, B. and D. Smith (Editors), Papers from the AAAI Spring Symposium on Logic-Based Program Synthesis: State of the Art and Future Trends, Stanford Univ., March 2002, AAAI Press SS02--05.
[10]
Gargantini, A. and C. Heitmeyer, "Using Model Checking to Generate Tests from Requirements Specifications", 7th European Software Engineering Conference/ACM SEN, Vol. 24, No. 6, November 1999, pp. 146--162.
[11]
Glass, R. L. "The Proof of Correctness Wars", Communications of the ACM, Vol. 45, No. 8 August 2002, pp. 19--21.
[12]
Khatib, L. and C. Pecheur (Editors), Papers from the AAAI Spring Symposium on Model-Based Validation of Intelligence, Stanford Univ, March 2001, AAAI Press SS01--04.
[13]
Ledeczi, A. and A. Bakay, M. Maroti, P. Volgyesi, G. Nordstrom, J. Sprinkle, E. Karsai, "Composing Domain Specific Design Environments", IEEE Computer, Vol. 34, No. 11, November 2001, pp. 44--51.
[14]
Lowry, M., "A Model for Software Reliability and the Impact of Program Synthesis", in {9}, pp. 77--80.
[15]
Mints, G., "Incomplete Proofs and Program Synthesis", in {9}, pp. 13--16.
[16]
Schumann, J., "Automatic Synthesis of Safety-Related Software", in {9}, pp. 105--108.
- Approximations, anomalies and "the proof of correctness wars"
Recommendations
Handling loops in bounded model checking of C programs via k-induction
The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative ...
An Assertional Proof of the Stability and Correctness of Natural Mergesort
We present a mechanically verified implementation of the sorting algorithm Natural Mergesort that consists of a few methods specified by their contracts of pre/post conditions. Methods are annotated with assertions that allow the automatic verification ...
An integrated environment for HDL verification
IVC '95: Proceedings of the 4th IEEE International Verilog HDL ConferenceThe functional verification of a digital design is an expensive step in the design process. As designs become more complex, simulation is challenged throughout the design and verification process, both at the low level (implementation verification), to ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2004 Author.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 March 2004
Published in SIGSOFT Volume 29, Issue 2
Check for updates
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 278Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 24 Jan 2025
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