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
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.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
K. Apt and E. R. Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag, 1991.
K. R. Apt, N. Francez, and S. Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2:226–241, 1988.
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.
C. Chou and E. Gafni. Understanding and verifying distributed algorithms using stratified decomposition. In Proceedings of 7th ACM PODC, pages 44–65, 1988.
T. Elrad and N. Francez. Decompositions of distributed programs into communication closed layers. Science of Computer Programming, 2(3):155–173, 1982.
N. Francez. Fairness. Springer-Verlag, 1986.
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.
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.
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.
S. Katz and D. Peled. Defining conditional independence using collapses. Theoretical Computer Science, 101:337–359, 1992.
S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6:107–120, 1992.
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.
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.
D. Peled. Combining partial order reductions with on-the-fly model checking. Journal of Formal Methods in System Design, 8:39–64, 1996.
D. Peled and A. Pnueli. Proving partial order properties. Theoretical Computer Science, 126:143–182, 1994.
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.
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.
P. Wolper and P. Godefroid. Partial-order methods for temporal verification. In Proceedings of CONCUR’93 (Eike Best, ed.), LNCS 715, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Glusman, M., Katz, S. (1999). Mechanizing Proofs of Computation Equivalence. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_31
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive