×

zbMATH — the first resource for mathematics

Automatic generation of invariants and intermediate assertions. (English) Zbl 0902.68120
Summary: Verifying temporal specifications of reactive and concurrent systems commonly relies on generating auxiliary assertions and on strengthening given properties of the system. This can be achieved by two dual approaches: The bottom-up method performs an abstract forward propagation (computation) of the system, generating auxiliary assertions; the top-down method performs an abstract backward propagation to strengthen given properties. Exact application of these methods is complete but is usually infeasible for large-scale verification. Approximation techniques are often needed to complete the verification. We give an overview of known methods for generation of auxiliary invariants in the verification of invariance properties. We extend these methods, by formalizing and analyzing a general verification rule that uses assertion graphs to generate auxiliary assertions for the verification of general safety properties.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
STeP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bensalem, S.; Lakhnech, Y.; Saidi, H., Powerful techniques for the automatic generation of invariants, (), 323-335
[2] Bjørner, N.; Browne, I.A.; Chang, E.; Colón, M.; Kapur, A.; Manna, Z.; Sipma, H.B.; Uribe, T.E., Tech. report STAN-CS-TR-95-1562, ()
[3] Bjørner, N.; Browne, I.A.; Manna, Z., Automatic generation of invariants and intermediate assertions, (), 589-623
[4] Chadha, R.; Plaisted, D.A., On the mechanical derivation of loop invariants, J. symbol. comput., 15, 5, 705-744, (1993) · Zbl 0804.68129
[5] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fix points, (), 238-252
[6] Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among the variables of a program, (), 84-97
[7] Dill, D.; Wong-Toi, H., Verification of real-time systems by successive over and under approximation, (), 409-422
[8] German, S.M.; Wegbreit, B., A synthesizer of inductive assertions, IEEE trans. software eng., 1, 68-75, (1975)
[9] Halbwachs, N.; Raymond, P.; Proy, Y.-E., Verification of linear hybrid systems by means of convex approximations, (), 223-237
[10] Harel, D., Statecharts: a visual approach to complex systems, () · Zbl 0637.68010
[11] Heintze, N., Set based program analysis, ()
[12] Henzinger, T.A.; Ho, P.-H., Algorithmic analysis of nonlinear hybrid systems, (), 225-238
[13] Jaffar, J.; Maher, M.J., Constraint logic programming: a survey, J. logic programming, 19-20, 3, 503-581, (1994)
[14] Karr, M., Affine relationships among variables of a program, Acta inform., 6, 133-151, (1976) · Zbl 0358.68025
[15] Katz, S.; Manna, Z., Logical analysis of programs, Comm. ACM, 19, 4, 188-206, (1976) · Zbl 0353.68016
[16] Lautenbach, K., Exacte bedingungen der lebendigkeit für eine klasse von Petri-netzen, (), 82 · Zbl 0298.68049
[17] Manna, Z.; Pnueli, A., Temporal verification of reactive systems: safety, (1995), Springer New York
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.