research-article

Mechanically Verifying Concurrent Programs with the Boyer-Moore Prove

Author:

D. M. GoldschlagAuthors Info & Claims

IEEE Transactions on Software Engineering, Volume 16, Issue 9

Pages 1005 - 1023

https://doi.org/10.1109/32.58787

Published: 01 September 1990 Publication History

Abstract

A proof system suitable for the mechanical verification of concurrent programs is described. This proof system is based on Unity, and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an operational semantics of the transition system model of concurrency. Proof rules are simply theorems of this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the underlying logic. Since this proof system essentially encodes Unity in another sound logic, and this encoding has been mechanically verified, this encoding proves the soundness of this formalization of Unity. This proof system has been mechanically verified by the Boyer-Moore prover. This proof system has been used to mechanically verify the correctness of a distributed algorithm that computes the minimum node value in a tree.

References

[1]

{1} B. Alpern and F. B. Schneider, "Defining liveness," Inform. Processing Lett., vol. 21, pp. 181-185, 1985.

[2]

{2} B. Alpern, A. J. Demers, and F. B. Schneider, "Safety without stuttering," Inform. Processing Lett., vol. 23, pp. 177-180, 1986.

Digital Library

[3]

{3} R. J. R. Back and J. von Wright, "Refinement concepts formalized in higher order logic," in IFIP TC2 Working Conf. Programming Concepts and Methods. M. Broy and C. B. Jones, Eds. Amsterdam, Elsevier, 1990.

[4]

{4} W. R. Bevier, "A library for hardware verification," Computational Logic, Inc., Austin, TX, Internal Note 57, 1988.

[5]

{5} R. S. Boyer and J. S. Moore, A Computational Logic. New York: Academic, 1979.

[6]

{6} R. S. Boyer and J. S. Moore, "Metafunctions: Proving them correct and using them efficiently as new proof procedures," in The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds. London: Academic, 1981.

[7]

{7} R. S. Boyer and J. S. Moore, A Computational Logic Handbook. Boston, MA: Academic, 1988.

[8]

{8} R. S. Boyer and J. S. Moore, "The addition of bounded quantification and partial functions to a computational logic and its theorem prover," Inst. Comput. Sci., Univ. Texas at Austin, Tech. Rep. ICSCA-CMP-52, Jan. 1988; also in J. Automated Reasoning, 1988; also available through Computational Logic, Inc., Austin, TX.

[9]

{9} R. S. Boyer, D. Goldschlag, M. Kaufmann, and J. S. Moore, "Functional instantiation in first order logic," Computational Logic, Inc., Austin, TX, Tech. Rep. 44, May 1989.

[10]

{10} M. C. Browne, E. M. Clarke, and D. L. Dill, "Automatic circuit verification using temporal logic: Two new examples," in Formal Aspects of VLSI Design, Proc. 1985 Edinburgh Workshop VLSI, G. J. Milne and P. A. Subrahmanyam, Eds. Amsterdam, The Netherlands: North-Holland, 1986, pp. 113-124.

[11]

{11} A. J. Camilleri, "Mechanizing CSP trace theory in higher order logic," IEEE Trans. Software Eng., this issue, pp. 993-1004.

[12]

{12} K. M. Chandy and J. Misra, Parallel Program Design: A Foundation. Reading, MA: Addison-Wesley, 1988.

Digital Library

[13]

{13} E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic," ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.

Digital Library

[14]

{14} D. L. Dill, Trace Theory for Automatic Hierarhical Verification of Speed-Independent Circuits. Cambridge, MA: MIT Press, 1988.

[15]

{15} D. M. Goldschlag, "Mechanizing unity," in IFIC TC2 Working Conf. Programming Concepts and Methods, M. Broy and C. B. Jones, Eds. Amsterdam, The Netherlands: Elsevier, 1990.

[16]

{16} M. Gordon, "HOL: A proof generating system for higher-order logic," Comput. Lab., Univ. Cambridge, Tech. Rep. 103, 1987.

[17]

{17} C. A. R. Hoare, "An axiomatic basis for computer programming," Commun. ACM, vol. 12, pp. 271-281, 1969.

Digital Library

[18]

{18} W. A. Hunt, Jr., "Microprocessor design verification," J. Automated Reasoning, 1989.

[19]

{19} C. S. Jutla, E. Knapp, and J. R. Rao, "Extensional semantics of parallel programs," Dep. Comput. Sci., Univ. Texas at Austin. Tech. Rep., Nov. 1988.

[20]

{20} M. Kaufmann, "A formal semantics and proof of soundness for the logic of the NQTHM version of the Boyer-Moore theorem prover," Inst. Comput. Sci., Univ. Texas at Austin, ICSCA Internal Note 229, 1986.

[21]

{21} M. Kaufmann, "A user's manual for an interative enhancement to the Boyer-Moore theorem prover," Inst. Comput. Sci., Univ. Texas at Austin, Tech. Rep. ICSCA-CMP-60, 1987; also available through Computational Logic, Inc., Austin, TX.

[22]

{22} M. Kaufmann, "DEFN-SK: An extension of the Boyer-Moore theorem prover to handle first-order quantifiers," draft, Computational Logic, Inc., Austin, TX, Tech. Rep. 43, May, 1989.

[23]

{23} L. Lamport, unpublished correspondence, DEC Systems Research Center, Palo Alto, CA, 1988.

[24]

{24} L. Lamport, "A simple approach to specifying concurrent systems," Commun. ACM, vol. 32, pp. 32-45, 1989.

Digital Library

[25]

{25} Z. Manna and A. Pnueli, "Adequate proof principles for invariance and liveness properties of concurrent programs," Sci. Comput. Program. , vol. 4, pp. 257-289, 1984.

Digital Library

[26]

{26} Z. Manna and A. Pnueli, "Verification of concurrent programs: The temporal framework," in The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds. London: Academic, 1981.

[27]

{27} D. M. Russinoff, "Verifying concurrent programs with the Boyer-Moore prover," MCC, Austin, TX, 1990.

[28]

{28} B. A. Sanders, "Stepwise refinement of mixed specifications of concurrent programs," in IFIP TC2 Working Conf. Programming Concepts and Methods, M. Broy and C. B. Jones, Eds. Amsterdam, The Netherlands: Elsevier, 1990.

[29]

{29} N. Shankar, "Proof checking metamathematics: Volumes I and II," Computational Logic, Inc., Austin, TX, Tech. Rep. 9, April, 1987.

[30]

{30} N. Shankar, "A mechanical proof of the Church-Rosser theorem," J. ACM, vol. 35, pp. 475-522, 1988.

Digital Library

[31]

{31} S. Sokolowski, "Soundness of Hoare's logic: An automatic proof using LCF," ACM Trans. Program. Lang. Syst., vol. 9, pp. 100- 120, 1987.

Digital Library

[32]

{32} G. L. Steele, Jr., Common Lisp The Language. Burlington, MA: Digital Press, 1984.

Cited By

Pendergrass JHuuck RKlein GSchlich B(2010)Verification of stack manipulation in the SCIP processorProceedings of the 5th international conference on Systems software verification10.5555/1929004.1929012(8-8)Online publication date: 6-Oct-2010
https://dl.acm.org/doi/10.5555/1929004.1929012
Stehr M(2008)Compositionality for Tightly Coupled Systems: A New Application of the Propositions-as-Types InterpretationFundamenta Informaticae10.5555/2365256.236525882:4(311-340)Online publication date: 1-Dec-2008
https://dl.acm.org/doi/10.5555/2365256.2365258
Stehr M(2008)Compositionality for Tightly Coupled Systems: A New Application of the Propositions-as-Types InterpretationFundamenta Informaticae10.5555/1366982.136698482:4(311-340)Online publication date: 1-Feb-2008
https://dl.acm.org/doi/10.5555/1366982.1366984
Show More Cited By

Index Terms

Mechanically Verifying Concurrent Programs with the Boyer-Moore Prove
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program verification
    2. Program semantics
      1. Operational semantics

Recommendations

A verification system for concurrent programs based on the Boyer-Moore prover
Abstract
We describe a mechanical proof system for concurrent programs, based on a formalization of the temporal framework of Manna and Pnueli as an extension of the computational logic of Boyer and Moore. The system provides a natural representation of ...
Some Inference Rules for Integer Arithmetic for Verification of Flowchart Programs on Integers

Significant modifications of the first-order rules have been developed so that they can be applied directly to algebraic expressions. The importance and implication of normalization of formulas in any theorem prover are discussed. It is shown how the ...
Mechanically verifying concurrent programs

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image IEEE Transactions on Software Engineering

IEEE Transactions on Software Engineering Volume 16, Issue 9

September 1990

175 pages

ISSN:0098-5589

Editor:
Victor R. Basili
Univ. of Maryland, College Park

Issue’s Table of Contents

Copyright © Copyright © 1990 IEEE. All Rights Reserved.

Publisher

IEEE Press

Publication History

Published: 01 September 1990

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pendergrass JHuuck RKlein GSchlich B(2010)Verification of stack manipulation in the SCIP processorProceedings of the 5th international conference on Systems software verification10.5555/1929004.1929012(8-8)Online publication date: 6-Oct-2010
https://dl.acm.org/doi/10.5555/1929004.1929012
Stehr M(2008)Compositionality for Tightly Coupled Systems: A New Application of the Propositions-as-Types InterpretationFundamenta Informaticae10.5555/2365256.236525882:4(311-340)Online publication date: 1-Dec-2008
https://dl.acm.org/doi/10.5555/2365256.2365258
Stehr M(2008)Compositionality for Tightly Coupled Systems: A New Application of the Propositions-as-Types InterpretationFundamenta Informaticae10.5555/1366982.136698482:4(311-340)Online publication date: 1-Feb-2008
https://dl.acm.org/doi/10.5555/1366982.1366984
Goldschlag D(1999)A Mechanization of Unity in PC-NQTHM-92Journal of Automated Reasoning10.1023/A:100626260912723:3(445-498)Online publication date: 1-Nov-1999
https://dl.acm.org/doi/10.1023/A%3A1006262609127
Chetali B(1998)Formal Verification of Concurrent Programs Using the Larch ProverIEEE Transactions on Software Engineering10.1109/32.66399724:1(46-62)Online publication date: 1-Jan-1998
https://dl.acm.org/doi/10.1109/32.663997
Staskauskas M(1996)An experience in the formal verification of industrial softwareCommunications of the ACM10.1145/272682.27271939:12es(256-es)Online publication date: 1-Dec-1996
https://dl.acm.org/doi/10.1145/272682.272719
Staskauskas M(1993)Formal Derivation of Concurrent ProgramsIEEE Transactions on Software Engineering10.1109/32.23201519:5(503-528)Online publication date: 1-May-1993
https://dl.acm.org/doi/10.1109/32.232015

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents