Abstract
The automated deduction and model checking communities have developed techniques that are impressively effective when applied to suitable problems. However, these problems seldom coincide exactly with those that arise in formal methods. Using small but realistic examples for illustration, I will argue that effective deductive support for formal methods requires cooperation among different techniques and an integrated approach to language, deduction, and supporting capabilities such as simulation and the construction of invariants and abstractions. Successful application of automated deduction to formal methods will enrich both fields, providing new opportunities for research and use of automated deduction, and making formal methods a truly useful and practical tool.
This work was supported by the Air Force Office of Scientific Research under contract F49620-95-C0044 and by the National Science Foundation under contract CCR-9509931. The applications described were undertaken for NASA Langley Research Center under contracts NAS1-18969 and NAS1-20334 and for ARPA through NASA Ames Research Center under contract NASA-NAG-2-891.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and T.A. Henzinger, editors. Computer-Aided Verification, CAV '96, Lecture Notes in Computer Science, New Brunswick, NJ, July 1996. Springer-Verlag.
S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful techniques for the automatic generation of invariants. In Alur and Henzinger [1].
R. S. Boyer and J S. Moore. Integrating decision procedures into heuristic theorem provers: A case study with linear arithmetic. In Machine Intelligence, volume 11. Oxford University Press, 1986.
David Cyrluk, Patrick Lincoln, and N. Shankar. On Shostak's decision procedure for combinations of theories. In International Conference on Automated Deduction (CADE)96, Lecture Notes in Computer Science, New Brunswick, NJ, July 1996. Springer-Verlag.
D.L. Dill, A.J. Hu, C.H. Yang, A. Drexler, R. Melton, S. Park, C.N. Ip, and U. Stern. The Murphi verification system. In Alur and Henzinger [1].
David Hamilton, Rick Covington, and John Kelly. Experiences in applying formal methods to the analysis of software and system requirements. In WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, pages 30–43, Boca Raton, FL, 1995. IEEE Computer Society.
Klaus Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe FME '96, number 1051 in Lecture Notes in Computer Science, pages 662–681, Oxford, UK, March 1996. Springer-Verlag.
C. B. Jones, K. D. Jones, P. A. Lindsay, and R. Moore. mural: A formal Development Support System. Springer-Verlag, London, UK, 1991.
L. Lamport and P. M. Melliar-Smith. Synchronizing clocks in the presence of faults. Journal of the ACM, 32(1):52–78, January 1985.
Mogens Nielsen, Klaus Havelund, Kim Ritter Wagner, and Chris George. The RAISE language, method and tools. Formal Aspects of Computing, 1(1):85–114, January-March 1989.
Sam Owre, John Rushby, and Natarajan Shankar. Analyzing tabular and statetransition specifications in PVS. Technical Report SRI-CSL-95-12, Computer Science Laboratory, SRI International, Menlo Park, CA, July 1995. Available, with specification files, from http://tiww.csl.sri.com/csl-95-12.html.
Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.
John Rushby. A formally verified algorithm for clock synchronization under a hybrid fault model. In Thirteenth ACM Symposium on Principles of Distributed Computing, pages 304–313, Los Angeles, CA, August 1994. Association for Computing Machinery.
John Rushby. Mechanizing formal methods: Opportunities and challenges. In Jonathan P. Bowen and Michael G. Hinchey, editors, ZUM '95: The Z Formal Specification Notation; 9th International Conference of Z Users, Volume 967 of Lecture Notes in Computer Science, pages 105–113, Limerick, Ireland, September 1995. Springer-Verlag.
John Rushby and Friedrich von Henke. Formal verification of algorithms for critical systems. IEEE Transactions on Software Engineering, 19(1):13–23, January 1993.
Robert E. Shostak. On the SUP-INF method for proving Presburger formulas. Journal of the ACM, 24(4):529–543, October 1977.
Mandayam K. Srivas and Steven P. Miller. Formal verification of the AAMP5 microprocessor. In Michael G. Hinchey and Jonathan P. Bowen, editors, Applications of Formal Methods, Prentice Hall International Series in Computer Science, chapter 7, pages 125–180. Prentice Hall, Hemel Hempstead, UK, 1995.
Gunnar M. N. Stålmarck. System for determining prepositional logic theorems by applying values and rules to triplets that are generated from Boolean formulae. United States Patent 5, 276,897, January 4 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rushby, J. (1996). Automated deduction and formal methods. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_67
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_67
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive