Abstract
I describe a systematic method for deductive verification of safety properties of concurrent programs. The method has much in common with the “verification diagrams” of Manna and Pnueli [17], but derives from different intuitions. It is based on the idea of strengthening a putative safety property into a disjunction of “configurations” that can easily be proved to be inductive. Transitions among the configurations have a natural diagrammatic representation that conveys insight into the operation of the program. The method lends itself to mechanization and is illustrated using a simplified version of an example that had defeated previous attempts at deductive verification.
This research was supported by DARPA through USAF Rome Laboratory Contract F30602-96-C-0204 and USAF Electronic Systems Center Contract F19628-96-C-0006, and by the National Science Foundation contract CCR-9509931.
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
Abdulla, P.A., Annichini, A., Bensalem, S., Bouajjani, A., Habermehl, P., Lakhnech, Y.: Verification of infinite-state systems by combining abstraction and reachability analysis. In: Halbwachs and Peled [11], pp. 146–159
Alur, R., Henzinger, T.A. (eds.): CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 319–331. Springer, Heidelberg (1998)
Bensalem, S., Lakhnech, Y., Saïdi, H.: Powerful techniques for the automatic generation of invariants. In: Alur and Henzinger [2], pp. 323–335
Bjørner, N., Browne, I.A., Manna, Z.: Automatic generation of invariants and intermediate assertions. Theoretical Computer Science 173(1), 49–87 (1997)
Bjørner, N., Lerner, U., Manna, Z.: Deductive verification of parameterized fault-tolerant systems: A case study. In: Second International Conference on Temporal Logic, ICTL 1997, Manchester, England (July 1997)
Browne, I.A., Manna, Z., Sipma, H.: Generalized temporal verification diagrams. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 484–498. Springer, Heidelberg (1995)
Creese, S.J., Roscoe, A.W.: TTP:A case study in combining induction and data independence. Technical Report PRG-TR-1-99, Oxford University Computing Laboratory. Oxford, England (1999)
Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs and Peled [11], pp. 160–171
de Alfaro, L., Manna, Z., Sipma, H.B., Uribe, T.E.: Visual verification of reactive systems. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 334–350. Springer, Heidelberg (1997)
Halbwachs, N., Peled, D.A. (eds.): CAV 1999. LNCS, vol. 1633. Springer, Heidelberg (1999)
Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 662–681. Springer, Heidelberg (1996)
Hosabettu, R., Srivas, M., Gopalakrishnan, G.: Proof of correctness of a processor with reorder buffer using the completion functions approach. In: Halbwachs and Peled [11], pp. 47–59
Katz, S., Lincoln, P., Rushby, J.: Low-overhead time-triggered group membership. In: Mavronicolas, M. (ed.) WDAG 1997. LNCS, vol. 1320, pp. 155–169. Springer, Heidelberg (1997)
Kopetz, H., Grünsteidl, G.: TTP—a protocol for fault-tolerant realtime systems. IEEE Computer 27(1), 14–23 (1994)
Manna, Z., Browne, A., Sipma, H.B., Uribe, T.E.: Visual abstractions for temporal verification. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 28–41. Springer, Heidelberg (1998)
Manna, Z., Pnueli, A.: Temporal verification diagrams. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 726–765. Springer, Heidelberg (1994)
Manna, Z., The STeP Group: STeP: Deductive-algorithmic verification of reactive and real-time systems. In: Alur and Henzinger [2], pp. 415–418
Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering 21(2), 107–125 (1995)
Park, S., Dill, D.L.: Verification of cache coherence protocols by aggregation of distributed transactions. Theory of Computing Systems 31(4), 355–376 (1998)
Pfeifer, H.: Formal verification of the TTA group membership algorithm (2000) (submitted for publication)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall International Series in Computer Science. Prentice Hall, Hemel Hempstead (1998)
Rushby, J.: Formal verification of a low-overhead group membership algorithm (2000) (in preparation)
Saïdi, H., Graf, S.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Saïdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs and Peled [11], pp. 443–454
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rushby, J. (2000). Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_38
Download citation
DOI: https://doi.org/10.1007/10722167_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive