Advertisement

Mechanizing Proofs of Computation Equivalence

  • Marcelo Glusman
  • Shmuel Katz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1633)

Abstract

A proof-theoretic mechanized verification environment that allows taking advantage of the “convenient computations” method is presented. The PV S theories encapsulating this method reduce the conceptual difficulty of proving a safety or liveness property for all the possible interleavings of a parallel computation by separating two different concerns: proving that certain convenient computations satisfy the property, and proving that every computation is related to a convenient one by a relation which preserves the property. We define one such relation, the equivalence of computations which differ only in the order of independent operations. We also introduce the computation as an explicit semantic object. The application of the method requires the definition of a “measure” function from computations into a well-founded set. We supply two possible default measures, which can be applied in many cases, together with examples of their use. The work is done in PV S, and a clear separation is made between “infrastructural” theories to be supplied as a proof environment library to users, and the specification and proof of particular examples.

Keywords

Model Check Computation Equivalence Execution Sequence Proof Obligation Independence Relation 
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

  1. 1.
    K. Apt and E. R. Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag, 1991.Google Scholar
  2. 2.
    K. R. Apt, N. Francez, and S. Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2:226–241, 1988.CrossRefGoogle Scholar
  3. 3.
    K.M. Chandy and L. Lamport. Distributed snapshots: determining global states of distributed systems. ACM Trans. on Computer Systems, 3(1):63–75, Feb 1985.CrossRefGoogle Scholar
  4. 4.
    C. Chou and E. Gafni. Understanding and verifying distributed algorithms using stratified decomposition. In Proceedings of 7th ACM PODC, pages 44–65, 1988.Google Scholar
  5. 5.
    T. Elrad and N. Francez. Decompositions of distributed programs into communication closed layers. Science of Computer Programming, 2(3):155–173, 1982.CrossRefGoogle Scholar
  6. 6.
    N. Francez. Fairness. Springer-Verlag, 1986.Google Scholar
  7. 7.
    P. Godefroid. On the costs and benefits of using partial-order methods for the verification of concurrent systems. In D. Peled, V. Pratt, and G. Holzmann, editors, Partial Order Methods in Verification, pages 289–303. American Mathematical Society, 1997. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29.Google Scholar
  8. 8.
    S. Katz. Refinement with global equivalence proofs in temporal logic. In D. Peled, V. Pratt, and G. Holzmann, editors, Partial Order Methods in Verification, pages 59–78. American Mathematical Society, 1997. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29.Google Scholar
  9. 9.
    S. Katz and D. Peled. Interleaving set temporal logic. Theoretical Computer Science, 75:263–287, 1990. Preliminary version was in the 6th ACM-PODC, 1987.MathSciNetCrossRefGoogle Scholar
  10. 10.
    S. Katz and D. Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101:337–359, 1992.MathSciNetCrossRefGoogle Scholar
  11. 11.
    S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6:107–120, 1992.MathSciNetCrossRefGoogle Scholar
  12. 12.
    S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer-Calvert. PVS Language Reference. Computer Science Lab, SRI International, Menlo Park, CA, 1998.Google Scholar
  13. 13.
    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.CrossRefGoogle Scholar
  14. 14.
    D. Peled. Combining partial order reductions with on-the-fly model checking. Journal of Formal Methods in System Design, 8:39–64, 1996.CrossRefGoogle Scholar
  15. 15.
    D. Peled and A. Pnueli. Proving partial order properties. Theoretical Computer Science, 126:143–182, 1994.MathSciNetCrossRefGoogle Scholar
  16. 16.
    D. Peled, V. Pratt, and G. Holzmann(eds.). Partial Order Methods in Verification. American Mathematical Society, 1997. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29.Google Scholar
  17. 17.
    John Rushby, Sam Owre, and N. Shankar. Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering, 24(9):709–720, September 1998.CrossRefGoogle Scholar
  18. 18.
    P. Wolper and P. Godefroid. Partial-order methods for temporal verification. In Proceedings of CONCUR’93 (Eike Best, ed.), LNCS 715, 1993.zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Marcelo Glusman
    • 1
  • Shmuel Katz
    • 1
  1. 1.Department of Computer ScienceThe TechnionHaifaIsrael

Personalised recommendations